# HG changeset patch # User wenzelm # Date 1183658499 -7200 # Node ID 361e9c3a5e3a7dcce975ac14e13742bf452d0380 # Parent 3a40294140f025d7eb5c9adc0f4116a67a6f740a tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal; diff -r 3a40294140f0 -r 361e9c3a5e3a src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Thu Jul 05 20:01:38 2007 +0200 +++ b/src/Pure/Isar/object_logic.ML Thu Jul 05 20:01:39 2007 +0200 @@ -20,11 +20,10 @@ val declare_atomize: attribute val declare_rulify: attribute val atomize_term: theory -> term -> term - val atomize_cterm: cterm -> thm - val atomize_thm: thm -> thm - val atomize_tac: int -> tactic + val atomize: conv + val atomize_prems: conv + val atomize_prems_tac: int -> tactic val full_atomize_tac: int -> tactic - val atomize_goal: int -> thm -> thm val rulify_term: theory -> term -> term val rulify_tac: int -> tactic val rulify: thm -> thm @@ -153,25 +152,19 @@ (* atomize *) -fun rewrite_prems_tac rews = - CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (MetaSimplifier.rewrite true rews))); - fun atomize_term thy = drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; -fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; -fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th; +fun atomize ct = + MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; -fun atomize_tac i st = - if Logic.has_meta_prems (Thm.prop_of st) i then - (rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st - else all_tac st; +fun atomize_prems ct = + if Logic.has_meta_prems (Thm.term_of ct) then + Conv.forall_conv ~1 (Conv.prems_conv ~1 atomize) ct + else Conv.all_conv ct; -fun full_atomize_tac i st = - MetaSimplifier.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st; - -fun atomize_goal i st = - (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st'); +val atomize_prems_tac = CONVERSION atomize_prems; +val full_atomize_tac = CONVERSION atomize; (* rulify *)