src/HOL/Import/proof_kernel.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26626 c6231d64d264
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -1277,10 +1277,10 @@
     1.4  	case get_hol4_mapping thyname thmname thy of
     1.5  	    SOME (SOME thmname) =>
     1.6  	    let
     1.7 -		val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
     1.8 +		val th1 = (SOME (PureThy.get_thm thy thmname)
     1.9  			   handle ERROR _ =>
    1.10  				  (case split_name thmname of
    1.11 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
    1.12 +				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
    1.13  							       handle _ => NONE)
    1.14  				     | NONE => NONE))
    1.15  	    in
    1.16 @@ -2158,17 +2158,10 @@
    1.17        add_dump ("syntax\n  "^n^" :: _ "^syn) thy
    1.18      end
    1.19  
    1.20 -(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
    1.21 -fun choose_upon_replay_history thy s dth =
    1.22 -    case Symtab.lookup (!type_intro_replay_history) s of
    1.23 -	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
    1.24 -      | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
    1.25 -*)
    1.26 -
    1.27  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
    1.28      case HOL4DefThy.get thy of
    1.29  	Replaying _ => (thy,
    1.30 -          HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
    1.31 +          HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
    1.32        | _ =>
    1.33  	let
    1.34              val _ = message "TYPE_INTRO:"