# HG changeset patch # User wenzelm # Date 1129651167 -7200 # Node ID f2fdd22accaa71f196edbaeb1fcc3722fc5916eb # Parent aef5a6d11c2ae483baf91b14da824e2b116372a1 Simplifier.theory_context; replaced get_const by Sign.the_const_type; eliminated obsolete sign_of; diff -r aef5a6d11c2a -r f2fdd22accaa src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Oct 18 17:59:26 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Oct 18 17:59:27 2005 +0200 @@ -385,27 +385,27 @@ let val ty = type_of rhs in - Logic.mk_equals (Const(Sign.intern_const (sign_of thy) name,ty),rhs) + Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs) end fun mk_teq name rhs thy = let val ty = type_of rhs in - HOLogic.mk_eq (Const(Sign.intern_const (sign_of thy) name,ty),rhs) + HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs) end fun intern_const_name thyname const thy = case get_hol4_const_mapping thyname const thy of SOME (_,cname,_) => cname | NONE => (case get_hol4_const_renaming thyname const thy of - SOME cname => Sign.intern_const (sign_of thy) (thyname ^ "." ^ cname) - | NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const)) + SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname) + | NONE => Sign.intern_const thy (thyname ^ "." ^ const)) fun intern_type_name thyname const thy = case get_hol4_type_mapping thyname const thy of SOME (_,cname) => cname - | NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const) + | NONE => Sign.intern_const thy (thyname ^ "." ^ const) fun mk_vartype name = TFree(name,["HOL.type"]) fun mk_thy_type thy Thy Tyop Args = Type(intern_type_name Thy Tyop thy,Args) @@ -418,23 +418,19 @@ fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) local - (* fun get_const sg thyname name = - (case term_of (read_cterm sg (name, TypeInfer.logicT)) of - c as Const _ => c) - handle _ => raise ERR "get_type" (name ^ ": No such constant")*) - fun get_const sg thyname name = - (case Sign.const_type sg name of - SOME ty => Const (name, ty) - | NONE => raise ERR "get_type" (name ^ ": No such constant")) + fun get_const sg thyname name = + (case Sign.const_type sg name of + SOME ty => Const (name, ty) + | NONE => raise ERR "get_type" (name ^ ": No such constant")) in fun prim_mk_const thy Thy Nam = let - val name = intern_const_name Thy Nam thy - val cmaps = HOL4ConstMaps.get thy + val name = intern_const_name Thy Nam thy + val cmaps = HOL4ConstMaps.get thy in - case StringPair.lookup cmaps (Thy,Nam) of - SOME(_,_,SOME ty) => Const(name,ty) - | _ => get_const (sign_of thy) Thy name + case StringPair.lookup cmaps (Thy,Nam) of + SOME(_,_,SOME ty) => Const(name,ty) + | _ => get_const thy Thy name end end @@ -985,8 +981,8 @@ local val th = thm "not_def" - val sg = sign_of_thm th - val pp = reflexive (cterm_of sg (Const("Trueprop",boolT-->propT))) + val thy = theory_of_thm th + val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT))) in val not_elim_thm = combination pp th end @@ -1231,18 +1227,15 @@ fun rewrite_hol4_term t thy = let - val sg = sign_of thy - - val hol4rews1 = map (Thm.transfer sg) (HOL4Rewrites.get thy) - val hol4ss = empty_ss setmksimps single addsimps hol4rews1 + val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) + val hol4ss = Simplifier.theory_context thy empty_ss + setmksimps single addsimps hol4rews1 in - Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t)) + Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t)) end fun get_isabelle_thm thyname thmname hol4conc thy = let - val sg = sign_of thy - val (info,hol4conc') = disamb_term hol4conc val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) val isaconc = @@ -1303,7 +1296,6 @@ val (a, b) = get_isabelle_thm thyname thmname hol4conc thy fun warn () = let - val sg = sign_of thy val (info,hol4conc') = disamb_term hol4conc val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) in @@ -1352,8 +1344,7 @@ fun intern_store_thm gen_output thyname thmname hth thy = let - val sg = sign_of thy - val (hth' as HOLThm (args as (_,th))) = norm_hthm sg hth + val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth val rew = rewrite_hol4_term (concl_of th) thy val th = equal_elim rew th val thy' = add_hol4_pending thyname thmname args thy @@ -1380,8 +1371,7 @@ let val _ = message "REFL:" val (info,tm') = disamb_term tm - val sg = sign_of thy - val ctm = Thm.cterm_of sg tm' + val ctm = Thm.cterm_of thy tm' val res = HOLThm(rens_of info,mk_REFL ctm) val _ = if_debug pth res in @@ -1392,8 +1382,7 @@ let val _ = message "ASSUME:" val (info,tm') = disamb_term tm - val sg = sign_of thy - val ctm = Thm.cterm_of sg (HOLogic.mk_Trueprop tm') + val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm') val th = Thm.trivial ctm val res = HOLThm(rens_of info,th) val _ = if_debug pth res @@ -1405,19 +1394,18 @@ let val _ = message "INST_TYPE:" val _ = if_debug pth hth - val sg = sign_of thy val tys_before = add_term_tfrees (prop_of th,[]) val th1 = varifyT th val tys_after = add_term_tvars (prop_of th1,[]) val tyinst = map (fn (bef, iS) => (case try (Lib.assoc (TFree bef)) lambda of - SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty) - | NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef)) + SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty) + | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef)) )) (zip tys_before tys_after) val res = Drule.instantiate (tyinst,[]) th1 val hth = HOLThm([],res) - val res = norm_hthm sg hth + val res = norm_hthm thy hth val _ = message "RESULT:" val _ = if_debug pth res in @@ -1429,10 +1417,9 @@ val _ = message "INST:" val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma val _ = if_debug pth hth - val sg = sign_of thy val (sdom,srng) = ListPair.unzip (rev sigma) val th = hthm2thm hth - val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th + val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th val res = HOLThm([],th1) val _ = message "RESULT:" val _ = if_debug pth res @@ -1466,7 +1453,7 @@ (thy,res) end -fun mk_COMB th1 th2 sg = +fun mk_COMB th1 th2 thy = let val (f,g) = case concl_of th1 of _ $ (Const("op =",_) $ f $ g) => (f,g) @@ -1477,9 +1464,9 @@ val fty = type_of f val (fd,fr) = dom_rng fty val comb_thm' = Drule.instantiate' - [SOME (ctyp_of sg fd),SOME (ctyp_of sg fr)] - [SOME (cterm_of sg f),SOME (cterm_of sg g), - SOME (cterm_of sg x),SOME (cterm_of sg y)] comb_thm + [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)] + [SOME (cterm_of thy f),SOME (cterm_of thy g), + SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm in [th1,th2] MRS comb_thm' end @@ -1494,10 +1481,9 @@ val (info1,ctxt') = disamb_term_from info ctxt val (info2,rews') = disamb_thms_from info1 rews - val sg = sign_of thy - val cctxt = cterm_of sg ctxt' + val cctxt = cterm_of thy ctxt' fun subst th [] = th - | subst th (rew::rews) = subst (mk_COMB th rew sg) rews + | subst th (rew::rews) = subst (mk_COMB th rew thy) rews val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th) val _ = message "RESULT:" val _ = if_debug pth res @@ -1512,14 +1498,13 @@ val (info,th) = disamb_thm hth val (info1,th1) = disamb_thm_from info hth1 val (info2,th2) = disamb_thm_from info1 hth2 - val sg = sign_of thy val th1 = norm_hyps th1 val th2 = norm_hyps th2 val (l,r) = case concl_of th of _ $ (Const("op |",_) $ l $ r) => (l,r) | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction" - val th1' = rearrange sg (HOLogic.mk_Trueprop l) th1 - val th2' = rearrange sg (HOLogic.mk_Trueprop r) th2 + val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1 + val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2 val res1 = th RS disj_cases_thm val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1 val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2 @@ -1537,8 +1522,7 @@ val _ = if_debug prin tm val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm - val sg = sign_of thy - val ct = Thm.cterm_of sg tm' + val ct = Thm.cterm_of thy tm' val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm val res = HOLThm(rens_of info',th RS disj1_thm') val _ = message "RESULT:" @@ -1554,8 +1538,7 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm - val sg = sign_of thy - val ct = Thm.cterm_of sg tm' + val ct = Thm.cterm_of thy tm' val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm val res = HOLThm(rens_of info',th RS disj2_thm') val _ = message "RESULT:" @@ -1648,13 +1631,12 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',[ex',wit']) = disamb_terms_from info [ex,wit] - val sg = sign_of thy - val cwit = cterm_of sg wit' + val cwit = cterm_of thy wit' val cty = ctyp_of_term cwit val a = case ex' of (Const("Ex",_) $ a) => a | _ => raise ERR "EXISTS" "Argument not existential" - val ca = cterm_of sg a + val ca = cterm_of thy a val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm) val th1 = beta_eta_thm th val th2 = implies_elim_all th1 @@ -1679,18 +1661,17 @@ | strip n (p::ps) th = strip (n-1) ps (implies_elim th (assume p)) | strip _ _ _ = raise ERR "CHOOSE" "strip error" - val sg = sign_of thy - val cv = cterm_of sg v' + val cv = cterm_of thy v' val th2 = norm_hyps th2 val cvty = ctyp_of_term cv val c = HOLogic.dest_Trueprop (concl_of th2) - val cc = cterm_of sg c + val cc = cterm_of thy c val a = case concl_of th1 of _ $ (Const("Ex",_) $ a) => a | _ => raise ERR "CHOOSE" "Conclusion not existential" - val ca = cterm_of (sign_of_thm th1) a + val ca = cterm_of (theory_of_thm th1) a val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm) - val th21 = rearrange sg (HOLogic.mk_Trueprop (a $ v')) th2 + val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2 val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21 val th23 = beta_eta_thm (forall_intr cv th22) val th11 = implies_elim_all (beta_eta_thm th1) @@ -1710,7 +1691,7 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',v') = disamb_term_from info v - val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy)) + val res = HOLThm(rens_of info',mk_GEN v' th thy) val _ = message "RESULT:" val _ = if_debug pth res in @@ -1724,8 +1705,7 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm - val sg = sign_of thy - val ctm = Thm.cterm_of sg tm' + val ctm = Thm.cterm_of thy tm' val cty = Thm.ctyp_of_term ctm val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm val th = th RS spec' @@ -1742,8 +1722,7 @@ val _ = if_debug pth hth1 val _ = if_debug pth hth2 val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val sg = sign_of thy - val res = HOLThm(rens_of info,mk_COMB th1 th2 sg) + val res = HOLThm(rens_of info,mk_COMB th1 th2 thy) val _ = message "RESULT:" val _ = if_debug pth res in @@ -1773,9 +1752,8 @@ val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm val th = norm_hyps th - val sg = sign_of thy - val ct = cterm_of sg tm' - val th1 = rearrange sg (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th + val ct = cterm_of thy tm' + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm' val res = HOLThm(rens_of info',res1) @@ -1785,15 +1763,15 @@ (thy,res) end -fun mk_ABS v th sg = +fun mk_ABS v th thy = let - val cv = cterm_of sg v + val cv = cterm_of thy v val th1 = implies_elim_all (beta_eta_thm th) val (f,g) = case concl_of th1 of _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g) | _ => raise ERR "mk_ABS" "Bad conclusion" val (fd,fr) = dom_rng (type_of f) - val abs_thm' = Drule.instantiate' [SOME (ctyp_of sg fd), SOME (ctyp_of sg fr)] [SOME (cterm_of sg f), SOME (cterm_of sg g)] abs_thm + val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm val th2 = forall_intr cv th1 val th3 = th2 COMP abs_thm' val res = implies_intr_hyps th3 @@ -1808,8 +1786,7 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',v') = disamb_term_from info v - val sg = sign_of thy - val res = HOLThm(rens_of info',mk_ABS v' th sg) + val res = HOLThm(rens_of info',mk_ABS v' th thy) val _ = message "RESULT:" val _ = if_debug pth res in @@ -1826,7 +1803,6 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',vlist') = disamb_terms_from info vlist - val sg = sign_of thy val th1 = case copt of SOME (c as Const(cname,cty)) => @@ -1843,14 +1819,14 @@ val cdom = fst (dom_rng (fst (dom_rng cty))) val vty = type_of v val newcty = inst_type cdom vty cty - val cc = cterm_of sg (Const(cname,newcty)) + val cc = cterm_of thy (Const(cname,newcty)) in - mk_COMB (mk_REFL cc) (mk_ABS v th sg) sg + mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy end) th vlist' end | SOME _ => raise ERR "GEN_ABS" "Bad constant" | NONE => - foldr (fn (v,th) => mk_ABS v th sg) th vlist' + foldr (fn (v,th) => mk_ABS v th thy) th vlist' val res = HOLThm(rens_of info',th1) val _ = message "RESULT:" val _ = if_debug pth res @@ -1862,12 +1838,11 @@ let val _ = message "NOT_INTRO:" val _ = if_debug pth hth - val sg = sign_of thy val th1 = implies_elim_all (beta_eta_thm th) val a = case concl_of th1 of _ $ (Const("op -->",_) $ a $ Const("False",_)) => a | _ => raise ERR "NOT_INTRO" "Conclusion of bad form" - val ca = cterm_of sg a + val ca = cterm_of thy a val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 val res = HOLThm(rens,implies_intr_hyps th2) val _ = message "RESULT:" @@ -1880,12 +1855,11 @@ let val _ = message "NOT_INTRO:" val _ = if_debug pth hth - val sg = sign_of thy val th1 = implies_elim_all (beta_eta_thm th) val a = case concl_of th1 of _ $ (Const("Not",_) $ a) => a | _ => raise ERR "NOT_ELIM" "Conclusion of bad form" - val ca = cterm_of sg a + val ca = cterm_of thy a val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 val res = HOLThm(rens,implies_intr_hyps th2) val _ = message "RESULT:" @@ -1902,10 +1876,9 @@ val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm val prems = prems_of th - val sg = sign_of thy val th1 = beta_eta_thm th val th2 = implies_elim_all th1 - val th3 = implies_intr (cterm_of sg (HOLogic.mk_Trueprop tm')) th2 + val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 val th4 = th3 COMP disch_thm val res = HOLThm(rens_of info',implies_intr_hyps th4) val _ = message "RESULT:" @@ -1919,8 +1892,7 @@ fun new_definition thyname constname rhs thy = let val constname = rename_const thyname thy constname - val sg = sign_of thy - val redeclared = isSome (Sign.const_type sg (Sign.intern_const sg constname)); + val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname)); val _ = warning ("Introducing constant " ^ constname) val (thmname,thy) = get_defname thyname constname thy val (info,rhs') = disamb_term rhs @@ -1934,24 +1906,23 @@ val def_thm = hd thms val thm' = def_thm RS meta_eq_to_obj_eq_thm val (thy',th) = (thy2, thm') - val fullcname = Sign.intern_const (sign_of thy') constname + val fullcname = Sign.intern_const thy' constname val thy'' = add_hol4_const_mapping thyname constname true fullcname thy' val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'') - val sg = sign_of thy'' val rew = rewrite_hol4_term eq thy'' - val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew))) + val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn then - add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy'' + add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy'' else - add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^ + add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) thy'' val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of SOME (_,res) => HOLThm(rens_of linfo,res) | NONE => raise ERR "new_definition" "Bad conclusion" - val fullname = Sign.full_name sg thmname + val fullname = Sign.full_name thy22 thmname val thy22' = case opt_get_output_thy thy22 of "" => add_hol4_mapping thyname thmname fullname thy22 | output_thy => @@ -1982,7 +1953,7 @@ val _ = if_debug pth hth val names = map (rename_const thyname thy) names val _ = warning ("Introducing constants " ^ (commafy names)) - val (HOLThm(rens,th)) = norm_hthm (sign_of thy) hth + val (HOLThm(rens,th)) = norm_hthm thy hth val thy1 = case HOL4DefThy.get thy of Replaying _ => thy | _ => @@ -2006,9 +1977,8 @@ in ((cname,cT,mk_syn thy cname)::cs,p) end) (([],HOLogic.dest_Trueprop (concl_of th)),names) - val sg = sign_of thy val str = Library.foldl (fn (acc,(c,T,csyn)) => - acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts) + acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts) val thy' = add_dump str thy in Theory.add_consts_i consts thy' @@ -2055,7 +2025,7 @@ fun to_isa_thm (hth as HOLThm(_,th)) = let - val (HOLThm args) = norm_hthm (sign_of_thm th) hth + val (HOLThm args) = norm_hthm (theory_of_thm th) hth in apsnd strip_shyps args end @@ -2076,7 +2046,7 @@ val _ = message "TYPE_DEF:" val _ = if_debug pth hth val _ = warning ("Introducing type " ^ tycname) - val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth + val (HOLThm(rens,td_th)) = norm_hthm thy hth val th2 = beta_eta_thm (td_th RS ex_imp_nonempty) val c = case concl_of th2 of _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c @@ -2089,18 +2059,16 @@ val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 - val fulltyname = Sign.intern_type (sign_of thy') tycname + val fulltyname = Sign.intern_type thy' tycname val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - val sg = sign_of thy'' - val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th3)) + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3)) val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") else () val thy4 = add_hol4_pending thyname thmname args thy'' - val sg = sign_of thy4 val rew = rewrite_hol4_term (concl_of td_th) thy4 - val th = equal_elim rew (Thm.transfer sg td_th) + val th = equal_elim rew (Thm.transfer thy4 td_th) val c = case HOLogic.dest_Trueprop (prop_of th) of Const("Ex",exT) $ P => let @@ -2115,7 +2083,7 @@ val proc_prop = if null tnames then smart_string_of_cterm else Library.setmp show_all_types true smart_string_of_cterm - val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of sg c)) ^ " " + val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ (Syntax.string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4 val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5 @@ -2162,13 +2130,12 @@ val _ = message "TYPE_INTRO:" val _ = if_debug pth hth val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")") - val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth - val sg = sign_of thy + val (HOLThm(rens,td_th)) = norm_hthm thy hth val tT = type_of t val light_nonempty' = - Drule.instantiate' [SOME (ctyp_of sg tT)] - [SOME (cterm_of sg P), - SOME (cterm_of sg t)] light_nonempty + Drule.instantiate' [SOME (ctyp_of thy tT)] + [SOME (cterm_of thy P), + SOME (cterm_of thy t)] light_nonempty val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty')) val c = case concl_of th2 of _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c @@ -2178,7 +2145,7 @@ val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) val (thy',typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy - val fulltyname = Sign.intern_type (sign_of thy') tycname + val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) val abs_ty = tT --> aty val rep_ty = aty --> tT @@ -2193,11 +2160,9 @@ val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' val _ = message "step 4" - val sg = sign_of thy'' - val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4)) + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) val thy4 = add_hol4_pending thyname thmname args thy'' - val sg = sign_of thy4 val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *) val c = let @@ -2213,11 +2178,11 @@ then smart_string_of_cterm else Library.setmp show_all_types true smart_string_of_cterm val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ - " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^ + " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ (Syntax.string_of_mixfix tsyn) ^ " morphisms "^ (quote rep_name)^" "^(quote abs_name)^"\n"^ (" apply (rule light_ex_imp_nonempty[where t="^ - (proc_prop (cterm_of sg t))^"])\n"^ + (proc_prop (cterm_of thy4 t))^"])\n"^ (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 val str_aty = string_of_ctyp (ctyp_of thy aty) val thy = add_dump_syntax thy rep_name