src/HOL/Modelcheck/mucke_oracle.ML
changeset 37146 f652333bbf8e
parent 37135 636e6d8645d6
child 37391 476270a6c2dc
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -487,7 +487,7 @@
     1.4          make_string sign (trm::list) =
     1.5             Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
     1.6  in
     1.7 -  PrintMode.setmp ["Mucke"] (make_string sign) terms
     1.8 +  Print_Mode.setmp ["Mucke"] (make_string sign) terms
     1.9  end;
    1.10  
    1.11  fun callmc s =