src/HOL/Import/proof_kernel.ML
changeset 17894 f2fdd22accaa
parent 17657 2f5f595eb618
child 17917 3c6e7760da89
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Oct 18 17:59:26 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Oct 18 17:59:27 2005 +0200
     1.3 @@ -385,27 +385,27 @@
     1.4      let
     1.5  	val ty = type_of rhs
     1.6      in
     1.7 -	Logic.mk_equals (Const(Sign.intern_const (sign_of thy) name,ty),rhs)
     1.8 +	Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
     1.9      end
    1.10  
    1.11  fun mk_teq name rhs thy =
    1.12      let
    1.13  	val ty = type_of rhs
    1.14      in
    1.15 -	HOLogic.mk_eq (Const(Sign.intern_const (sign_of thy) name,ty),rhs)
    1.16 +	HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
    1.17      end
    1.18  
    1.19  fun intern_const_name thyname const thy =
    1.20      case get_hol4_const_mapping thyname const thy of
    1.21  	SOME (_,cname,_) => cname
    1.22        | NONE => (case get_hol4_const_renaming thyname const thy of
    1.23 -		     SOME cname => Sign.intern_const (sign_of thy) (thyname ^ "." ^ cname)
    1.24 -		   | NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const))
    1.25 +		     SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
    1.26 +		   | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
    1.27  
    1.28  fun intern_type_name thyname const thy =
    1.29      case get_hol4_type_mapping thyname const thy of
    1.30  	SOME (_,cname) => cname
    1.31 -      | NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const)
    1.32 +      | NONE => Sign.intern_const thy (thyname ^ "." ^ const)
    1.33  
    1.34  fun mk_vartype name = TFree(name,["HOL.type"])
    1.35  fun mk_thy_type thy Thy Tyop Args = Type(intern_type_name Thy Tyop thy,Args)
    1.36 @@ -418,23 +418,19 @@
    1.37  fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
    1.38  
    1.39  local 
    1.40 -    (* fun get_const sg thyname name = 
    1.41 -       (case term_of (read_cterm sg (name, TypeInfer.logicT)) of
    1.42 -          c as Const _ => c)
    1.43 -       handle _ => raise ERR "get_type" (name ^ ": No such constant")*)
    1.44 -      fun get_const sg thyname name = 
    1.45 -       (case Sign.const_type sg name of
    1.46 -          SOME ty => Const (name, ty)
    1.47 -        | NONE => raise ERR "get_type" (name ^ ": No such constant"))
    1.48 +  fun get_const sg thyname name = 
    1.49 +    (case Sign.const_type sg name of
    1.50 +      SOME ty => Const (name, ty)
    1.51 +    | NONE => raise ERR "get_type" (name ^ ": No such constant"))
    1.52  in
    1.53  fun prim_mk_const thy Thy Nam =
    1.54      let
    1.55 -	val name = intern_const_name Thy Nam thy
    1.56 -	val cmaps = HOL4ConstMaps.get thy
    1.57 +      val name = intern_const_name Thy Nam thy
    1.58 +      val cmaps = HOL4ConstMaps.get thy
    1.59      in
    1.60 -	case StringPair.lookup cmaps (Thy,Nam) of
    1.61 -	    SOME(_,_,SOME ty) => Const(name,ty)
    1.62 -	  | _ => get_const (sign_of thy) Thy name
    1.63 +      case StringPair.lookup cmaps (Thy,Nam) of
    1.64 +        SOME(_,_,SOME ty) => Const(name,ty)
    1.65 +      | _ => get_const thy Thy name
    1.66      end
    1.67  end
    1.68  
    1.69 @@ -985,8 +981,8 @@
    1.70  
    1.71  local
    1.72      val th = thm "not_def"
    1.73 -    val sg = sign_of_thm th
    1.74 -    val pp = reflexive (cterm_of sg (Const("Trueprop",boolT-->propT)))
    1.75 +    val thy = theory_of_thm th
    1.76 +    val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
    1.77  in
    1.78  val not_elim_thm = combination pp th
    1.79  end
    1.80 @@ -1231,18 +1227,15 @@
    1.81  
    1.82  fun rewrite_hol4_term t thy =
    1.83      let
    1.84 -	val sg = sign_of thy
    1.85 -
    1.86 -	val hol4rews1 = map (Thm.transfer sg) (HOL4Rewrites.get thy)
    1.87 -	val hol4ss = empty_ss setmksimps single addsimps hol4rews1
    1.88 +	val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
    1.89 +	val hol4ss = Simplifier.theory_context thy empty_ss
    1.90 +          setmksimps single addsimps hol4rews1
    1.91      in
    1.92 -	Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
    1.93 +	Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
    1.94      end
    1.95  
    1.96  fun get_isabelle_thm thyname thmname hol4conc thy =
    1.97      let
    1.98 -	val sg = sign_of thy
    1.99 -
   1.100  	val (info,hol4conc') = disamb_term hol4conc
   1.101  	val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
   1.102  	val isaconc =
   1.103 @@ -1303,7 +1296,6 @@
   1.104      val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
   1.105      fun warn () =
   1.106          let
   1.107 -            val sg = sign_of thy		     
   1.108  	    val (info,hol4conc') = disamb_term hol4conc
   1.109  	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
   1.110  	in
   1.111 @@ -1352,8 +1344,7 @@
   1.112  
   1.113  fun intern_store_thm gen_output thyname thmname hth thy =
   1.114      let
   1.115 -	val sg = sign_of thy
   1.116 -	val (hth' as HOLThm (args as (_,th))) = norm_hthm sg hth
   1.117 +	val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
   1.118  	val rew = rewrite_hol4_term (concl_of th) thy
   1.119  	val th  = equal_elim rew th
   1.120  	val thy' = add_hol4_pending thyname thmname args thy
   1.121 @@ -1380,8 +1371,7 @@
   1.122      let
   1.123  	val _ = message "REFL:"
   1.124  	val (info,tm') = disamb_term tm
   1.125 -	val sg = sign_of thy
   1.126 -	val ctm = Thm.cterm_of sg tm'
   1.127 +	val ctm = Thm.cterm_of thy tm'
   1.128  	val res = HOLThm(rens_of info,mk_REFL ctm)
   1.129  	val _ = if_debug pth res
   1.130      in
   1.131 @@ -1392,8 +1382,7 @@
   1.132      let
   1.133  	val _ = message "ASSUME:"
   1.134  	val (info,tm') = disamb_term tm
   1.135 -	val sg = sign_of thy
   1.136 -	val ctm = Thm.cterm_of sg (HOLogic.mk_Trueprop tm')
   1.137 +	val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm')
   1.138  	val th = Thm.trivial ctm
   1.139  	val res = HOLThm(rens_of info,th)
   1.140  	val _ = if_debug pth res
   1.141 @@ -1405,19 +1394,18 @@
   1.142      let
   1.143  	val _ = message "INST_TYPE:"
   1.144  	val _ = if_debug pth hth
   1.145 -	val sg = sign_of thy
   1.146  	val tys_before = add_term_tfrees (prop_of th,[])
   1.147  	val th1 = varifyT th
   1.148  	val tys_after = add_term_tvars (prop_of th1,[])
   1.149  	val tyinst = map (fn (bef, iS) =>
   1.150  			     (case try (Lib.assoc (TFree bef)) lambda of
   1.151 -				  SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty)
   1.152 -				| NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef))
   1.153 +				  SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
   1.154 +				| NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
   1.155  			     ))
   1.156  			 (zip tys_before tys_after)
   1.157  	val res = Drule.instantiate (tyinst,[]) th1
   1.158  	val hth = HOLThm([],res)
   1.159 -	val res = norm_hthm sg hth
   1.160 +	val res = norm_hthm thy hth
   1.161  	val _ = message "RESULT:"
   1.162  	val _ = if_debug pth res
   1.163      in
   1.164 @@ -1429,10 +1417,9 @@
   1.165  	val _ = message "INST:"
   1.166  	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
   1.167  	val _ = if_debug pth hth
   1.168 -	val sg = sign_of thy
   1.169  	val (sdom,srng) = ListPair.unzip (rev sigma)
   1.170  	val th = hthm2thm hth
   1.171 -	val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th
   1.172 +	val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th
   1.173  	val res = HOLThm([],th1)
   1.174  	val _ = message "RESULT:"
   1.175  	val _ = if_debug pth res
   1.176 @@ -1466,7 +1453,7 @@
   1.177  	(thy,res)
   1.178      end
   1.179  
   1.180 -fun mk_COMB th1 th2 sg =
   1.181 +fun mk_COMB th1 th2 thy =
   1.182      let
   1.183  	val (f,g) = case concl_of th1 of
   1.184  			_ $ (Const("op =",_) $ f $ g) => (f,g)
   1.185 @@ -1477,9 +1464,9 @@
   1.186  	val fty = type_of f
   1.187  	val (fd,fr) = dom_rng fty
   1.188  	val comb_thm' = Drule.instantiate'
   1.189 -			    [SOME (ctyp_of sg fd),SOME (ctyp_of sg fr)]
   1.190 -			    [SOME (cterm_of sg f),SOME (cterm_of sg g),
   1.191 -			     SOME (cterm_of sg x),SOME (cterm_of sg y)] comb_thm
   1.192 +			    [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
   1.193 +			    [SOME (cterm_of thy f),SOME (cterm_of thy g),
   1.194 +			     SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm
   1.195      in
   1.196  	[th1,th2] MRS comb_thm'
   1.197      end
   1.198 @@ -1494,10 +1481,9 @@
   1.199  	val (info1,ctxt') = disamb_term_from info ctxt
   1.200  	val (info2,rews') = disamb_thms_from info1 rews
   1.201  
   1.202 -	val sg = sign_of thy
   1.203 -	val cctxt = cterm_of sg ctxt'
   1.204 +	val cctxt = cterm_of thy ctxt'
   1.205  	fun subst th [] = th
   1.206 -	  | subst th (rew::rews) = subst (mk_COMB th rew sg) rews
   1.207 +	  | subst th (rew::rews) = subst (mk_COMB th rew thy) rews
   1.208  	val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th)
   1.209  	val _ = message "RESULT:"
   1.210  	val _ = if_debug pth res
   1.211 @@ -1512,14 +1498,13 @@
   1.212  	val (info,th) = disamb_thm hth
   1.213  	val (info1,th1) = disamb_thm_from info hth1
   1.214  	val (info2,th2) = disamb_thm_from info1 hth2
   1.215 -	val sg = sign_of thy
   1.216  	val th1 = norm_hyps th1
   1.217  	val th2 = norm_hyps th2
   1.218  	val (l,r) = case concl_of th of
   1.219  			_ $ (Const("op |",_) $ l $ r) => (l,r)
   1.220  		      | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
   1.221 -	val th1' = rearrange sg (HOLogic.mk_Trueprop l) th1
   1.222 -	val th2' = rearrange sg (HOLogic.mk_Trueprop r) th2
   1.223 +	val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
   1.224 +	val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
   1.225  	val res1 = th RS disj_cases_thm
   1.226  	val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1
   1.227  	val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2
   1.228 @@ -1537,8 +1522,7 @@
   1.229  	val _ = if_debug prin tm
   1.230  	val (info,th) = disamb_thm hth
   1.231  	val (info',tm') = disamb_term_from info tm
   1.232 -	val sg = sign_of thy
   1.233 -	val ct = Thm.cterm_of sg tm'
   1.234 +	val ct = Thm.cterm_of thy tm'
   1.235  	val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm
   1.236  	val res = HOLThm(rens_of info',th RS disj1_thm')
   1.237  	val _ = message "RESULT:"
   1.238 @@ -1554,8 +1538,7 @@
   1.239  	val _ = if_debug pth hth
   1.240  	val (info,th) = disamb_thm hth
   1.241  	val (info',tm') = disamb_term_from info tm
   1.242 -	val sg = sign_of thy
   1.243 -	val ct = Thm.cterm_of sg tm'
   1.244 +	val ct = Thm.cterm_of thy tm'
   1.245  	val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm
   1.246  	val res = HOLThm(rens_of info',th RS disj2_thm')
   1.247  	val _ = message "RESULT:"
   1.248 @@ -1648,13 +1631,12 @@
   1.249  	val _ = if_debug pth hth
   1.250  	val (info,th) = disamb_thm hth
   1.251  	val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
   1.252 -	val sg = sign_of thy
   1.253 -	val cwit = cterm_of sg wit'
   1.254 +	val cwit = cterm_of thy wit'
   1.255  	val cty = ctyp_of_term cwit
   1.256  	val a = case ex' of
   1.257  		    (Const("Ex",_) $ a) => a
   1.258  		  | _ => raise ERR "EXISTS" "Argument not existential"
   1.259 -	val ca = cterm_of sg a
   1.260 +	val ca = cterm_of thy a
   1.261  	val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
   1.262  	val th1 = beta_eta_thm th
   1.263  	val th2 = implies_elim_all th1
   1.264 @@ -1679,18 +1661,17 @@
   1.265  	  | strip n (p::ps) th =
   1.266  	    strip (n-1) ps (implies_elim th (assume p))
   1.267  	  | strip _ _ _ = raise ERR "CHOOSE" "strip error"
   1.268 -	val sg = sign_of thy
   1.269 -	val cv = cterm_of sg v'
   1.270 +	val cv = cterm_of thy v'
   1.271  	val th2 = norm_hyps th2
   1.272  	val cvty = ctyp_of_term cv
   1.273  	val c = HOLogic.dest_Trueprop (concl_of th2)
   1.274 -	val cc = cterm_of sg c
   1.275 +	val cc = cterm_of thy c
   1.276  	val a = case concl_of th1 of
   1.277  		    _ $ (Const("Ex",_) $ a) => a
   1.278  		  | _ => raise ERR "CHOOSE" "Conclusion not existential"
   1.279 -	val ca = cterm_of (sign_of_thm th1) a
   1.280 +	val ca = cterm_of (theory_of_thm th1) a
   1.281  	val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
   1.282 -	val th21 = rearrange sg (HOLogic.mk_Trueprop (a $ v')) th2
   1.283 +	val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
   1.284  	val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
   1.285  	val th23 = beta_eta_thm (forall_intr cv th22)
   1.286  	val th11 = implies_elim_all (beta_eta_thm th1)
   1.287 @@ -1710,7 +1691,7 @@
   1.288  	val _ = if_debug pth hth
   1.289  	val (info,th) = disamb_thm hth
   1.290  	val (info',v') = disamb_term_from info v
   1.291 -	val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy))
   1.292 +	val res = HOLThm(rens_of info',mk_GEN v' th thy)
   1.293  	val _ = message "RESULT:"
   1.294  	val _ = if_debug pth res
   1.295      in
   1.296 @@ -1724,8 +1705,7 @@
   1.297  	val _ = if_debug pth hth
   1.298  	val (info,th) = disamb_thm hth
   1.299  	val (info',tm') = disamb_term_from info tm
   1.300 -	val sg = sign_of thy
   1.301 -	val ctm = Thm.cterm_of sg tm'
   1.302 +	val ctm = Thm.cterm_of thy tm'
   1.303  	val cty = Thm.ctyp_of_term ctm
   1.304  	val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm
   1.305  	val th = th RS spec'
   1.306 @@ -1742,8 +1722,7 @@
   1.307  	val _ = if_debug pth hth1
   1.308  	val _ = if_debug pth hth2
   1.309  	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
   1.310 -	val sg = sign_of thy
   1.311 -	val res = HOLThm(rens_of info,mk_COMB th1 th2 sg)
   1.312 +	val res = HOLThm(rens_of info,mk_COMB th1 th2 thy)
   1.313  	val _ = message "RESULT:"
   1.314  	val _ = if_debug pth res
   1.315      in
   1.316 @@ -1773,9 +1752,8 @@
   1.317  	val (info,th) = disamb_thm hth
   1.318  	val (info',tm') = disamb_term_from info tm
   1.319  	val th = norm_hyps th
   1.320 -	val sg = sign_of thy
   1.321 -	val ct = cterm_of sg tm'
   1.322 -	val th1 = rearrange sg (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
   1.323 +	val ct = cterm_of thy tm'
   1.324 +	val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
   1.325  	val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
   1.326  	val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
   1.327  	val res = HOLThm(rens_of info',res1)
   1.328 @@ -1785,15 +1763,15 @@
   1.329  	(thy,res)
   1.330      end
   1.331  
   1.332 -fun mk_ABS v th sg =
   1.333 +fun mk_ABS v th thy =
   1.334      let
   1.335 -	val cv = cterm_of sg v
   1.336 +	val cv = cterm_of thy v
   1.337  	val th1 = implies_elim_all (beta_eta_thm th)
   1.338  	val (f,g) = case concl_of th1 of
   1.339  			_ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
   1.340  		      | _ => raise ERR "mk_ABS" "Bad conclusion"
   1.341  	val (fd,fr) = dom_rng (type_of f)
   1.342 -	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
   1.343 +	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
   1.344  	val th2 = forall_intr cv th1
   1.345  	val th3 = th2 COMP abs_thm'
   1.346  	val res = implies_intr_hyps th3
   1.347 @@ -1808,8 +1786,7 @@
   1.348  	val _ = if_debug pth hth
   1.349  	val (info,th) = disamb_thm hth
   1.350  	val (info',v') = disamb_term_from info v
   1.351 -	val sg = sign_of thy
   1.352 -	val res = HOLThm(rens_of info',mk_ABS v' th sg)
   1.353 +	val res = HOLThm(rens_of info',mk_ABS v' th thy)
   1.354  	val _ = message "RESULT:"
   1.355  	val _ = if_debug pth res
   1.356      in
   1.357 @@ -1826,7 +1803,6 @@
   1.358  	val _ = if_debug pth hth
   1.359  	val (info,th) = disamb_thm hth
   1.360  	val (info',vlist') = disamb_terms_from info vlist
   1.361 -	val sg = sign_of thy
   1.362  	val th1 =
   1.363  	    case copt of
   1.364  		SOME (c as Const(cname,cty)) =>
   1.365 @@ -1843,14 +1819,14 @@
   1.366  				  val cdom = fst (dom_rng (fst (dom_rng cty)))
   1.367  				  val vty  = type_of v
   1.368  				  val newcty = inst_type cdom vty cty
   1.369 -				  val cc = cterm_of sg (Const(cname,newcty))
   1.370 +				  val cc = cterm_of thy (Const(cname,newcty))
   1.371  			      in
   1.372 -				  mk_COMB (mk_REFL cc) (mk_ABS v th sg) sg
   1.373 +				  mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
   1.374  			      end) th vlist'
   1.375  		end
   1.376  	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
   1.377  	      | NONE => 
   1.378 -		foldr (fn (v,th) => mk_ABS v th sg) th vlist'
   1.379 +		foldr (fn (v,th) => mk_ABS v th thy) th vlist'
   1.380  	val res = HOLThm(rens_of info',th1)
   1.381  	val _ = message "RESULT:"
   1.382  	val _ = if_debug pth res
   1.383 @@ -1862,12 +1838,11 @@
   1.384      let
   1.385  	val _ = message "NOT_INTRO:"
   1.386  	val _ = if_debug pth hth
   1.387 -	val sg = sign_of thy
   1.388  	val th1 = implies_elim_all (beta_eta_thm th)
   1.389  	val a = case concl_of th1 of
   1.390  		    _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
   1.391  		  | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
   1.392 -	val ca = cterm_of sg a
   1.393 +	val ca = cterm_of thy a
   1.394  	val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
   1.395  	val res = HOLThm(rens,implies_intr_hyps th2)
   1.396  	val _ = message "RESULT:"
   1.397 @@ -1880,12 +1855,11 @@
   1.398      let
   1.399  	val _ = message "NOT_INTRO:"
   1.400  	val _ = if_debug pth hth
   1.401 -	val sg = sign_of thy
   1.402  	val th1 = implies_elim_all (beta_eta_thm th)
   1.403  	val a = case concl_of th1 of
   1.404  		    _ $ (Const("Not",_) $ a) => a
   1.405  		  | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
   1.406 -	val ca = cterm_of sg a
   1.407 +	val ca = cterm_of thy a
   1.408  	val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
   1.409  	val res = HOLThm(rens,implies_intr_hyps th2)
   1.410  	val _ = message "RESULT:"
   1.411 @@ -1902,10 +1876,9 @@
   1.412  	val (info,th) = disamb_thm hth
   1.413  	val (info',tm') = disamb_term_from info tm
   1.414  	val prems = prems_of th
   1.415 -	val sg = sign_of thy
   1.416  	val th1 = beta_eta_thm th
   1.417  	val th2 = implies_elim_all th1
   1.418 -	val th3 = implies_intr (cterm_of sg (HOLogic.mk_Trueprop tm')) th2
   1.419 +	val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
   1.420  	val th4 = th3 COMP disch_thm
   1.421  	val res = HOLThm(rens_of info',implies_intr_hyps th4)
   1.422  	val _ = message "RESULT:"
   1.423 @@ -1919,8 +1892,7 @@
   1.424  fun new_definition thyname constname rhs thy =
   1.425      let
   1.426  	val constname = rename_const thyname thy constname
   1.427 -        val sg = sign_of thy
   1.428 -        val redeclared = isSome (Sign.const_type sg (Sign.intern_const sg constname));
   1.429 +        val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
   1.430  	val _ = warning ("Introducing constant " ^ constname)
   1.431  	val (thmname,thy) = get_defname thyname constname thy
   1.432  	val (info,rhs') = disamb_term rhs
   1.433 @@ -1934,24 +1906,23 @@
   1.434  	val def_thm = hd thms
   1.435  	val thm' = def_thm RS meta_eq_to_obj_eq_thm
   1.436  	val (thy',th) = (thy2, thm')
   1.437 -	val fullcname = Sign.intern_const (sign_of thy') constname
   1.438 +	val fullcname = Sign.intern_const thy' constname
   1.439  	val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
   1.440  	val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
   1.441 -	val sg = sign_of thy''
   1.442  	val rew = rewrite_hol4_term eq thy''
   1.443 -	val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew)))
   1.444 +	val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
   1.445  	val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
   1.446  		    then
   1.447 -			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''
   1.448 +			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''
   1.449  		    else
   1.450 -			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^
   1.451 +			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
   1.452  				  "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
   1.453  				 thy''
   1.454  
   1.455  	val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
   1.456  		     SOME (_,res) => HOLThm(rens_of linfo,res)
   1.457  		   | NONE => raise ERR "new_definition" "Bad conclusion"
   1.458 -	val fullname = Sign.full_name sg thmname
   1.459 +	val fullname = Sign.full_name thy22 thmname
   1.460  	val thy22' = case opt_get_output_thy thy22 of
   1.461  			 "" => add_hol4_mapping thyname thmname fullname thy22
   1.462  		       | output_thy =>
   1.463 @@ -1982,7 +1953,7 @@
   1.464  	    val _ = if_debug pth hth
   1.465  	    val names = map (rename_const thyname thy) names
   1.466  	    val _ = warning ("Introducing constants " ^ (commafy names))
   1.467 -	    val (HOLThm(rens,th)) = norm_hthm (sign_of thy) hth
   1.468 +	    val (HOLThm(rens,th)) = norm_hthm thy hth
   1.469  	    val thy1 = case HOL4DefThy.get thy of
   1.470  			   Replaying _ => thy
   1.471  			 | _ =>
   1.472 @@ -2006,9 +1977,8 @@
   1.473  							  in
   1.474  							      ((cname,cT,mk_syn thy cname)::cs,p)
   1.475  							  end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
   1.476 -			       val sg = sign_of thy
   1.477  			       val str = Library.foldl (fn (acc,(c,T,csyn)) =>
   1.478 -						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
   1.479 +						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
   1.480  			       val thy' = add_dump str thy
   1.481  			   in
   1.482  			       Theory.add_consts_i consts thy'
   1.483 @@ -2055,7 +2025,7 @@
   1.484  				      
   1.485  fun to_isa_thm (hth as HOLThm(_,th)) =
   1.486      let
   1.487 -	val (HOLThm args) = norm_hthm (sign_of_thm th) hth
   1.488 +	val (HOLThm args) = norm_hthm (theory_of_thm th) hth
   1.489      in
   1.490  	apsnd strip_shyps args
   1.491      end
   1.492 @@ -2076,7 +2046,7 @@
   1.493  	    val _ = message "TYPE_DEF:"
   1.494  	    val _ = if_debug pth hth
   1.495  	    val _ = warning ("Introducing type " ^ tycname)
   1.496 -	    val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth
   1.497 +	    val (HOLThm(rens,td_th)) = norm_hthm thy hth
   1.498  	    val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
   1.499  	    val c = case concl_of th2 of
   1.500  			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
   1.501 @@ -2089,18 +2059,16 @@
   1.502  				      
   1.503  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
   1.504  
   1.505 -	    val fulltyname = Sign.intern_type (sign_of thy') tycname
   1.506 +	    val fulltyname = Sign.intern_type thy' tycname
   1.507  	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   1.508  
   1.509 -	    val sg = sign_of thy''
   1.510 -	    val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th3))
   1.511 +	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
   1.512  	    val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
   1.513  		    else ()
   1.514  	    val thy4 = add_hol4_pending thyname thmname args thy''
   1.515  
   1.516 -	    val sg = sign_of thy4
   1.517  	    val rew = rewrite_hol4_term (concl_of td_th) thy4
   1.518 -	    val th  = equal_elim rew (Thm.transfer sg td_th)
   1.519 +	    val th  = equal_elim rew (Thm.transfer thy4 td_th)
   1.520  	    val c   = case HOLogic.dest_Trueprop (prop_of th) of
   1.521  			  Const("Ex",exT) $ P =>
   1.522  			  let
   1.523 @@ -2115,7 +2083,7 @@
   1.524  	    val proc_prop = if null tnames
   1.525  			    then smart_string_of_cterm
   1.526  			    else Library.setmp show_all_types true smart_string_of_cterm
   1.527 -	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of sg c)) ^ " " 
   1.528 +	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " 
   1.529  				 ^ (Syntax.string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
   1.530  	    
   1.531  	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
   1.532 @@ -2162,13 +2130,12 @@
   1.533              val _ = message "TYPE_INTRO:"
   1.534  	    val _ = if_debug pth hth
   1.535  	    val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
   1.536 -	    val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth
   1.537 -	    val sg = sign_of thy
   1.538 +	    val (HOLThm(rens,td_th)) = norm_hthm thy hth
   1.539  	    val tT = type_of t
   1.540  	    val light_nonempty' =
   1.541 -		Drule.instantiate' [SOME (ctyp_of sg tT)]
   1.542 -				   [SOME (cterm_of sg P),
   1.543 -				    SOME (cterm_of sg t)] light_nonempty
   1.544 +		Drule.instantiate' [SOME (ctyp_of thy tT)]
   1.545 +				   [SOME (cterm_of thy P),
   1.546 +				    SOME (cterm_of thy t)] light_nonempty
   1.547  	    val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
   1.548  	    val c = case concl_of th2 of
   1.549  			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
   1.550 @@ -2178,7 +2145,7 @@
   1.551  	    val tsyn = mk_syn thy tycname
   1.552  	    val typ = (tycname,tnames,tsyn)
   1.553  	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
   1.554 -	    val fulltyname = Sign.intern_type (sign_of thy') tycname
   1.555 +	    val fulltyname = Sign.intern_type thy' tycname
   1.556  	    val aty = Type (fulltyname, map mk_vartype tnames)
   1.557  	    val abs_ty = tT --> aty
   1.558  	    val rep_ty = aty --> tT
   1.559 @@ -2193,11 +2160,9 @@
   1.560  	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
   1.561              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   1.562              val _ = message "step 4"
   1.563 -	    val sg = sign_of thy''
   1.564 -	    val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4))
   1.565 +	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
   1.566  	    val thy4 = add_hol4_pending thyname thmname args thy''
   1.567  	   
   1.568 -	    val sg = sign_of thy4
   1.569  	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
   1.570  	    val c   =
   1.571  		let
   1.572 @@ -2213,11 +2178,11 @@
   1.573  			    then smart_string_of_cterm
   1.574  			    else Library.setmp show_all_types true smart_string_of_cterm
   1.575  	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
   1.576 -              " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^ 
   1.577 +              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ 
   1.578  	      (Syntax.string_of_mixfix tsyn) ^ " morphisms "^
   1.579                (quote rep_name)^" "^(quote abs_name)^"\n"^ 
   1.580  	      ("  apply (rule light_ex_imp_nonempty[where t="^
   1.581 -              (proc_prop (cterm_of sg t))^"])\n"^              
   1.582 +              (proc_prop (cterm_of thy4 t))^"])\n"^              
   1.583  	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
   1.584  	    val str_aty = string_of_ctyp (ctyp_of thy aty)
   1.585              val thy = add_dump_syntax thy rep_name