src/Pure/assumption.ML
changeset 21605 4e7307e229b3
parent 21577 3ff126ca39b4
child 21679 06715e253686
     1.1 --- a/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
     1.2 +++ b/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  *)
     1.5  fun presume_export _ = assume_export false;
     1.6  
     1.7 -val assume = norm_hhf o Thm.assume;
     1.8 +val assume = MetaSimplifier.norm_hhf o Thm.assume;
     1.9  
    1.10  
    1.11  
    1.12 @@ -100,9 +100,9 @@
    1.13  
    1.14  fun export is_goal inner outer =
    1.15    let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
    1.16 -    norm_hhf_protect
    1.17 +    MetaSimplifier.norm_hhf_protect
    1.18      #> fold_rev (fn (e, As) => e is_goal As) asms
    1.19 -    #> norm_hhf_protect
    1.20 +    #> MetaSimplifier.norm_hhf_protect
    1.21    end;
    1.22  
    1.23  fun export_morphism inner outer =