2197 Drule.instantiate' |
2197 Drule.instantiate' |
2198 [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] |
2198 [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] |
2199 [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] |
2199 [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] |
2200 typedef_hol2hollight |
2200 typedef_hol2hollight |
2201 val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' |
2201 val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' |
2202 val _ = if Drule.tvars_of th4 = [] then () else raise ERR "type_introduction" "no type variables expected any more" |
2202 val _ = null (Drule.fold_terms Term.add_tvars th4 []) orelse |
2203 val _ = if Drule.vars_of th4 = [] then () else raise ERR "type_introduction" "no term variables expected any more" |
2203 raise ERR "type_introduction" "no type variables expected any more" |
|
2204 val _ = null (Drule.fold_terms Term.add_vars th4 []) orelse |
|
2205 raise ERR "type_introduction" "no term variables expected any more" |
2204 val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) |
2206 val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) |
2205 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' |
2207 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' |
2206 val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname |
2208 val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname |
2207 val _ = message "step 4" |
2209 val _ = message "step 4" |
2208 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) |
2210 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) |