remove Theory.new_specification and reimplement new_definition

in terms of the revised Thm.prim_specification. obviously this breaks
anything that depended on Theory.new_specification, so the next job is
to rework those things (and write a backwards-compatible version, but
later in the build sequence because it needs pairs.)

src/0/Thm.sml

@@ -1099,11 +1099,9 @@ fun mk_defn_thm (witness_tag, c) =
 fun ERR f msg = HOL_ERR {origin_structure = "Thm",
                          origin_function = f, message = msg}
 val TYDEF_ERR = ERR "prim_type_definition"
-val DEF_ERR   = ERR "new_definition"
-val SPEC_ERR  = ERR "new_specification"
+val SPEC_ERR  = ERR "prim_specification"
 
 val TYDEF_FORM_ERR = TYDEF_ERR "expected a theorem of the form \"?x. P x\""
-val DEF_FORM_ERR   = DEF_ERR   "expected a term of the form \"v = M\""
 
 (* some simple term manipulation functions *)
 fun mk_exists (absrec as (Bvar,_)) =
@@ -1183,6 +1181,8 @@ in
 end
 
 (* subsumed by prim_specification
+val DEF_ERR   = ERR "new_definition"
+val DEF_FORM_ERR   = DEF_ERR   "expected a term of the form \"v = M\""
 fun prim_constant_definition Thy M = let
   val (lhs, rhs) = with_exn dest_eq M DEF_FORM_ERR
   val {Name, Thy, Ty} =

src/postkernel/Theory.sig

@@ -76,8 +76,8 @@ sig
   structure Definition : sig
     val new_type_definition    : string * thm -> thm
     val loose_specification    : string * thm -> thm
+
     val new_definition         : string * term -> thm
-    val new_specification      : string * string list * thm -> thm
 
     val new_definition_hook    : ((term -> term list * term) *
                                   (term list * thm -> thm)) ref

src/postkernel/Theory.sml

@@ -1081,32 +1081,17 @@ fun loose_specification(name, th) = let
  end
  handle e => raise (wrap_exn "Definition" "loose_specification" e);
 
-(* TODO: implement these two in terms of the above
-
 fun new_definition(name,M) =
  let val (dest,post) = !new_definition_hook
-     val (V,eq)      = dest M
-     val def_th      = Thm.prim_constant_definition (current_theory()) eq
-     val {Name,Thy,...} = dest_thy_const (rand (rator (concl def_th)))
+     val (V,eq)          = dest M
+     val Thy             = current_theory()
+     val ([Name],def_th) = Thm.prim_specification Thy (Thm.ASSUME eq)
  in
    store_definition (name, post(V,def_th)) before
    call_hooks (TheoryDelta.NewConstant{Name=Name, Thy=Thy})
  end
  handle e => raise (wrap_exn "Definition" "new_definition" e);
 
-fun new_specification (name, cnames, th) = let
-  val thy   = current_theory()
-  val def   = Thm.prim_specification thy cnames th
-  val final = store_definition (name, def)
- in
-  List.app (fn s => call_hooks (TheoryDelta.NewConstant{Name=s, Thy = thy}))
-           cnames
-  ; final
- end
- handle e => raise (wrap_exn "Definition" "new_specification" e);
-
-*)
-
 end (* Definition struct *)
 
 end (* Theory *)