disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
eliminated obsolete Sign.cert_def;
misc tuning and clarification;

--- a/src/Pure/more_thm.ML	Sat Mar 27 16:01:45 2010 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 27 17:36:32 2010 +0100
@@ -347,21 +347,30 @@
 fun add_axiom (b, prop) thy =
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
     val thy' =
       Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b');
-    val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
+    val thm =
+      Thm.instantiate (recover, []) axm'
+      |> unvarify_global
+      |> fold elim_implies of_sorts;
   in (thm, thy') end;
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
-    val (strip, recover, prop') = stripped_sorts thy prop;
-    val thy' = Theory.add_def unchecked overloaded (b, prop') thy;
+    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
+    val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
+    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b);
-    val thm = unvarify_global (Thm.instantiate (recover, []) axm');
+    val thm =
+      Thm.instantiate (recover, []) axm'
+      |> unvarify_global
+      |> fold_rev Thm.implies_intr prems;
   in (thm, thy') end;
 
 

--- a/src/Pure/sign.ML	Sat Mar 27 16:01:45 2010 +0100
+++ b/src/Pure/sign.ML	Sat Mar 27 17:36:32 2010 +0100
@@ -68,7 +68,6 @@
   val cert_prop: theory -> term -> term
   val no_frees: Pretty.pp -> term -> term
   val no_vars: Pretty.pp -> term -> term
-  val cert_def: Proof.context -> term -> (string * typ) * term
   val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (binding * int * mixfix) list -> theory -> theory
@@ -332,14 +331,6 @@
 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
 
-fun cert_def ctxt tm =
-  let val ((lhs, rhs), _) = tm
-    |> no_vars (Syntax.pp ctxt)
-    |> Logic.strip_imp_concl
-    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
-  in (Term.dest_Const (Term.head_of lhs), rhs) end
-  handle TERM (msg, _) => error msg;
-
 
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)

--- a/src/Pure/theory.ML	Sat Mar 27 16:01:45 2010 +0100
+++ b/src/Pure/theory.ML	Sat Mar 27 17:36:32 2010 +0100
@@ -240,7 +240,9 @@
   let
     val ctxt = ProofContext.init thy;
     val name = Sign.full_name thy b;
-    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
+    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
+      handle TERM (msg, _) => error msg;
+    val lhs_const = Term.dest_Const (Term.head_of lhs);
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end