src/HOL/Import/proof_kernel.ML
changeset 22709 9ab51bac6287
parent 22691 290454649b8c
child 24630 351a308ab58d
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -473,10 +473,10 @@
     1.4  val check_name_thy = theory "Main"
     1.5  
     1.6  fun valid_boundvarname s =
     1.7 -  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
     1.8 +  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
     1.9  
    1.10  fun valid_varname s =
    1.11 -  can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
    1.12 +  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
    1.13  
    1.14  fun protect_varname s =
    1.15      if innocent_varname s andalso valid_varname s then s else