src/HOL/Mutabelle/mutabelle_extra.ML
changeset 35625 9c818cab0dd0
parent 35537 59dd6be5834c
child 36255 f8b3381e1437
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -91,7 +91,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) (Mutabelle.freeze t));
    1.10  
    1.11  fun invoke_quickcheck quickcheck_generator thy t =