# HG changeset patch # User wenzelm # Date 965690279 -7200 # Node ID c2e3773475b6c9788219419af74375e49cd29f45 # Parent e3981c1f769df7f3afb20023a846f876b2d22766 norm_hhf results; diff -r e3981c1f769d -r c2e3773475b6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Aug 08 01:17:28 2000 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Aug 08 01:17:59 2000 +0200 @@ -49,6 +49,7 @@ val generalizeT: context -> context -> typ -> typ val generalize: context -> context -> term -> term val find_free: term -> string -> term option + val norm_hhf: thm -> thm val export_wrt: bool -> context -> context option -> (thm -> thm Seq.seq) * (int -> tactic) list val auto_bind_goal: term -> context -> context val auto_bind_facts: string -> term list -> context -> context @@ -652,19 +653,23 @@ val generalize = Term.map_term_types oo generalizeT; -(* export theorems *) + +(** export theorems **) fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None | get_free _ (opt, _) = opt; fun find_free t x = foldl_aterms (get_free x) (None, t); +val norm_hhf = + Drule.forall_elim_vars_safe o Tactic.rewrite_rule [Drule.norm_hhf_eq]; + local fun export tfrees fixes goal_asms thm = thm - |> Drule.forall_elim_vars 0 + |> norm_hhf |> Seq.EVERY (rev (map op |> goal_asms)) |> Seq.map (fn rule => let @@ -673,7 +678,7 @@ in rule |> Drule.forall_intr_list frees - |> Drule.forall_elim_vars 0 + |> norm_hhf |> Drule.tvars_intr_list tfrees end); @@ -892,7 +897,7 @@ val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); val cprops = map (Thm.cterm_of (sign_of ctxt')) props; - val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops; + val asms = map (norm_hhf o Drule.assume_goal) cprops; val ths = map (fn th => ([th], [])) asms; val (ctxt'', [(_, thms)]) =