src/HOL/Import/proof_kernel.ML
changeset 20286 4cf8e86a2d29
parent 19998 c8018518e112
child 20483 04aa552a83bc
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Aug 02 18:33:46 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Aug 02 22:26:37 2006 +0200
     1.3 @@ -2199,8 +2199,10 @@
     1.4  		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
     1.5                      typedef_hol2hollight
     1.6  	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
     1.7 -            val _ = if Drule.tvars_of th4 = [] then () else raise ERR "type_introduction" "no type variables expected any more" 
     1.8 -            val _ = if Drule.vars_of th4 = [] then () else raise ERR "type_introduction" "no term variables expected any more"
     1.9 +            val _ = null (Drule.fold_terms Term.add_tvars th4 []) orelse
    1.10 +              raise ERR "type_introduction" "no type variables expected any more"
    1.11 +            val _ = null (Drule.fold_terms Term.add_vars th4 []) orelse
    1.12 +              raise ERR "type_introduction" "no term variables expected any more"
    1.13  	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
    1.14              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.15  	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname