src/Pure/Isar/local_defs.ML
changeset 22900 f8a7c10e1bd0
parent 22846 fb79144af9a3
child 23541 f8c5e218e4d8
     1.1 --- a/src/Pure/Isar/local_defs.ML	Wed May 09 23:28:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu May 10 00:39:45 2007 +0200
     1.3 @@ -171,10 +171,10 @@
     1.4    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
     1.5      (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
     1.6  
     1.7 -val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
     1.8 +val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite;
     1.9  
    1.10  fun meta_rewrite_tac ctxt i =
    1.11 -  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
    1.12 +  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (meta_rewrite ctxt)));
    1.13  
    1.14  
    1.15  (* rewriting with object-level rules *)