# HG changeset patch
# User wenzelm
# Date 1160353202 -7200
# Node ID 7132ab2b4621a35323b3475d11e59add8e703f3a
# Parent  5f7458cc4f67dfcba9f0ea0c8072a20549c9421e
simplified derived_def;

diff -r 5f7458cc4f67 -r 7132ab2b4621 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Oct 09 02:20:01 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Mon Oct 09 02:20:02 2006 +0200
@@ -24,7 +24,7 @@
   val fold: Proof.context -> thm list -> thm -> thm
   val fold_tac: Proof.context -> thm list -> tactic
   val derived_def: Proof.context -> bool -> term ->
-    ((string * typ) * term) * (Proof.context -> term -> thm -> thm)
+    ((string * typ) * term) * (Proof.context -> thm -> thm)
 end;
 
 structure LocalDefs: LOCAL_DEFS =
@@ -164,13 +164,12 @@
       |> (snd o Logic.dest_equals o Thm.prop_of)
       |> K conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt);
-    fun prove ctxt' lhs def =   (* FIXME check/simplify *)
+    fun prove ctxt' def =
       let
-        val prop' = Term.subst_atomic [(Free (c, T), lhs)] prop;   (* FIXME !? *)
         val frees = Term.fold_aterms (fn Free (x, _) =>
-          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
+          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
       in
-        Goal.prove ctxt' frees [] prop' (K (ALLGOALS
+        Goal.prove ctxt' frees [] prop (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
             Tactic.rewrite_goal_tac [def] THEN'
             Tactic.resolve_tac [Drule.reflexive_thm])))