src/HOL/Import/proof_kernel.ML
changeset 26336 a0e2b706ce73
parent 24976 821628d16552
child 26343 0dd2eab7b296
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Mar 19 22:27:57 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 (Name thmname))
     1.8 +		val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
     1.9  			   handle ERROR _ =>
    1.10  				  (case split_name thmname of
    1.11 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
    1.12 +				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
    1.13  							       handle _ => NONE)
    1.14  				     | NONE => NONE))
    1.15  	    in
    1.16 @@ -2168,7 +2168,7 @@
    1.17  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
    1.18      case HOL4DefThy.get thy of
    1.19  	Replaying _ => (thy,
    1.20 -          HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
    1.21 +          HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
    1.22        | _ =>
    1.23  	let
    1.24              val _ = message "TYPE_INTRO:"