# 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])))