src/HOL/Mutabelle/mutabelle.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 35845 e5980f0ad025
     1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -494,7 +494,7 @@
     1.4  fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
     1.5   | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
     1.6  
     1.7 -fun preprocess thy insts t = ObjectLogic.atomize_term thy
     1.8 +fun preprocess thy insts t = Object_Logic.atomize_term thy
     1.9   (map_types (inst_type insts) (freeze t));
    1.10  
    1.11  fun is_executable thy insts th =