src/HOL/Import/proof_kernel.ML

 	  | G 3 = Library.setmp show_brackets true (G 2)
           | G _ = raise SMART_STRING 
 	fun F n =
 	    let
 		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
-		val cu  = read_cterm thy (str,T)
+		val cu  = Thm.read_cterm thy (str,T)
 	    in
 		if match cu
 		then quote str
 		else F (n+1)
 	    end

 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
 
 val check_name_thy = theory "Main"
 
 fun valid_boundvarname s =
-  can (fn () => read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
+  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
 
 fun valid_varname s =
-  can (fn () => read_cterm check_name_thy (s, TypeInfer.logicT)) ();
+  can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
 
 fun protect_varname s =
     if innocent_varname s andalso valid_varname s then s else
     case Symtab.lookup (!protected_varnames) s of
       SOME t => t