src/HOL/Modelcheck/MuckeSyn.thy

 (* extension with removing bold font (TH) *)
 fun mk_lam_def (_::_) _ _ = NONE  
   | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
     let val thy = theory_of_thm t;
-	val fnam = Sign.string_of_term thy (getfun LHS);
-	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
+	val fnam = Syntax.string_of_term_global thy (getfun LHS);
+	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
     in
 	SOME (prove_goal thy gl (fn prems =>
   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
     end