changeset 13197 | 0567f4fd1415 |
parent 12829 | c92128238f85 |
child 13334 | 27149d72bdff |
--- a/src/Pure/Isar/object_logic.ML Fri May 31 18:48:31 2002 +0200 +++ b/src/Pure/Isar/object_logic.ML Fri May 31 18:49:31 2002 +0200 @@ -129,7 +129,7 @@ (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews))))); fun atomize_term sg = - drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg); + drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) []; fun atomize_tac i st = if Logic.has_meta_prems (Thm.prop_of st) i then