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 =