src/Pure/assumption.ML
changeset 41228 e1fce873b814
parent 39557 fe5722fce758
child 41552 c5e71fee3617
     1.1 --- a/src/Pure/assumption.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/Pure/assumption.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  *)
     1.5  fun presume_export _ = assume_export false;
     1.6  
     1.7 -val assume = MetaSimplifier.norm_hhf o Thm.assume;
     1.8 +val assume = Raw_Simplifier.norm_hhf o Thm.assume;
     1.9  
    1.10  
    1.11  
    1.12 @@ -110,9 +110,9 @@
    1.13  (* export *)
    1.14  
    1.15  fun export is_goal inner outer =
    1.16 -  MetaSimplifier.norm_hhf_protect #>
    1.17 +  Raw_Simplifier.norm_hhf_protect #>
    1.18    fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
    1.19 -  MetaSimplifier.norm_hhf_protect;
    1.20 +  Raw_Simplifier.norm_hhf_protect;
    1.21  
    1.22  fun export_term inner outer =
    1.23    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);