# HG changeset patch # User wenzelm # Date 1138664383 -3600 # Node ID ceb93f3af7f03c898fd319e7cf78a9e4c3bb8fa7 # Parent c4b4fbd74ffb57c07b08302d0563df6a02b91778 advanced translations: Context.generic; tuned; diff -r c4b4fbd74ffb -r ceb93f3af7f0 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jan 31 00:39:40 2006 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Jan 31 00:39:43 2006 +0100 @@ -277,16 +277,16 @@ (Symtab.merge (K true) (extfields1,extfields2)) (Symtab.merge (K true) (fieldext1,fieldext2)); - fun print sg ({records = recs, ...}: record_data) = + fun print thy ({records = recs, ...}: record_data) = let - val prt_typ = Sign.pretty_typ sg; + val prt_typ = Sign.pretty_typ thy; fun pretty_parent NONE = [] | pretty_parent (SOME (Ts, name)) = [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]]; fun pretty_field (c, T) = Pretty.block - [Pretty.str (Sign.extern_const sg c), Pretty.str " ::", + [Pretty.str (Sign.extern_const thy c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)]; fun pretty_record (name, {args, parent, fields, ...}: record_info) = @@ -356,7 +356,7 @@ splits extfields fieldext; in RecordsData.put data thy end; -fun get_extinjects sg = #extinjects (RecordsData.get sg); +fun get_extinjects thy = #extinjects (RecordsData.get thy); (* access 'extsplit' *) @@ -404,7 +404,7 @@ val get_extfields = Symtab.lookup o #extfields o RecordsData.get; -fun get_extT_fields sg T = +fun get_extT_fields thy T = let val ((name,Ts),moreT) = dest_recT T; val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name) @@ -412,19 +412,19 @@ val midx = maxidx_of_typs (moreT::Ts); fun varify (a, S) = TVar ((a, midx), S); val varifyT = map_type_tfree varify; - val {records,extfields,...} = RecordsData.get sg; + val {records,extfields,...} = RecordsData.get thy; val (flds,(more,_)) = split_last (Symtab.lookup_multi extfields name); val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); - val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0); + val (subst,_) = fold (Sign.typ_unify thy) (but_last args ~~ but_last Ts) (Vartab.empty,0); val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds; in (flds',(more,moreT)) end; -fun get_recT_fields sg T = +fun get_recT_fields thy T = let - val (root_flds,(root_more,root_moreT)) = get_extT_fields sg T; + val (root_flds,(root_more,root_moreT)) = get_extT_fields thy T; val (rest_flds,rest_more) = - if is_recT root_moreT then get_recT_fields sg root_moreT + if is_recT root_moreT then get_recT_fields thy root_moreT else ([],(root_more,root_moreT)); in (root_flds@rest_flds,rest_more) end; @@ -507,8 +507,9 @@ else [dest_ext_field mark trm] | dest_ext_fields _ mark t = [dest_ext_field mark t] -fun gen_ext_fields_tr sep mark sfx more sg t = +fun gen_ext_fields_tr sep mark sfx more context t = let + val thy = Context.theory_of context; val msg = "error in record input: "; val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = @@ -521,8 +522,8 @@ | splitargs _ _ = ([],[]); fun mk_ext (fargs as (name,arg)::_) = - (case get_fieldext sg (Sign.intern_const sg name) of - SOME (ext,_) => (case get_extfields sg ext of + (case get_fieldext thy (Sign.intern_const thy name) of + SOME (ext,_) => (case get_extfields thy ext of SOME flds => let val (args,rest) = splitargs (map fst (but_last flds)) fargs; @@ -536,8 +537,9 @@ in mk_ext fieldargs end; -fun gen_ext_type_tr sep mark sfx more sg t = +fun gen_ext_type_tr sep mark sfx more context t = let + val thy = Context.theory_of context; val msg = "error in record-type input: "; val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = @@ -549,16 +551,16 @@ | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([],[]); - fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg); + fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); - fun to_type t = Sign.certify_typ sg - (Sign.intern_typ sg + fun to_type t = Sign.certify_typ thy + (Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)); fun mk_ext (fargs as (name,arg)::_) = - (case get_fieldext sg (Sign.intern_const sg name) of + (case get_fieldext thy (Sign.intern_const thy name) of SOME (ext,alphas) => - (case get_extfields sg ext of + (case get_extfields thy ext of SOME flds => (let val flds' = but_last flds; @@ -566,7 +568,7 @@ val (args,rest) = splitargs (map fst flds') fargs; val vartypes = map Type.varifyT types; val argtypes = map to_type args; - val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes) + val (subst,_) = fold (Sign.typ_unify thy) (vartypes ~~ argtypes) (Vartab.empty,0); val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o Envir.norm_type subst o Type.varifyT) @@ -582,20 +584,20 @@ in mk_ext fieldargs end; -fun gen_adv_record_tr sep mark sfx unit sg [t] = - gen_ext_fields_tr sep mark sfx unit sg t +fun gen_adv_record_tr sep mark sfx unit context [t] = + gen_ext_fields_tr sep mark sfx unit context t | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); -fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = - gen_ext_fields_tr sep mark sfx more sg t +fun gen_adv_record_scheme_tr sep mark sfx context [t, more] = + gen_ext_fields_tr sep mark sfx more context t | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); -fun gen_adv_record_type_tr sep mark sfx unit sg [t] = - gen_ext_type_tr sep mark sfx unit sg t +fun gen_adv_record_type_tr sep mark sfx unit context [t] = + gen_ext_type_tr sep mark sfx unit context t | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); -fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = - gen_ext_type_tr sep mark sfx more sg t +fun gen_adv_record_type_scheme_tr sep mark sfx context [t, more] = + gen_ext_type_tr sep mark sfx more context t | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit; @@ -640,18 +642,19 @@ let val name_sfx = suffix sfx name in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; -fun record_tr' sep mark record record_scheme unit sg t = +fun record_tr' sep mark record record_scheme unit context t = let + val thy = Context.theory_of context; fun field_lst t = (case strip_comb t of (Const (ext,_),args as (_::_)) - => (case try (unsuffix extN) (Sign.intern_const sg ext) of + => (case try (unsuffix extN) (Sign.intern_const thy ext) of SOME ext' - => (case get_extfields sg ext' of + => (case get_extfields thy ext' of SOME flds => (let val (f::fs) = but_last (map fst flds); - val flds' = Sign.extern_const sg f :: map NameSpace.base fs; + val flds' = Sign.extern_const thy f :: map NameSpace.base fs; val (args',more) = split_last args; in (flds'~~args')@field_lst more end handle UnequalLengths => [("",t)]) @@ -672,7 +675,7 @@ fun gen_record_tr' name = let val name_sfx = suffix extN name; val unit = (fn Const ("Unity",_) => true | _ => false); - fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg + fun tr' context ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit context (list_comb (Syntax.const name_sfx,ts)) in (name_sfx,tr') end @@ -682,12 +685,13 @@ (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *) (* the (nested) extension types. *) -fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm = +fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context tm = let + val thy = Context.theory_of context; (* tm is term representation of a (nested) field type. We first reconstruct the *) (* type from tm so that we can continue on the type level rather then the term level.*) - fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg); + fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); (* WORKAROUND: * If a record type occurs in an error message of type inference there @@ -699,19 +703,19 @@ * fixT works around. *) fun fixT (T as Type (x,[])) = - if String.isPrefix "??'" x then TFree (x,Sign.defaultS sg) else T + if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T | fixT (Type (x,xs)) = Type (x,map fixT xs) | fixT T = T; - val T = fixT (Sign.intern_typ sg + val T = fixT (Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); fun mk_type_abbr subst name alphas = - let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas); + let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS thy)) alphas); in Syntax.term_of_typ (! Syntax.show_sorts) - (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end; + (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end; - fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0)); + fun unify rT T = fst (Sign.typ_unify thy (Type.varifyT rT,T) (Vartab.empty,0)); in if !print_record_type_abbr then (case last_extT T of @@ -721,39 +725,40 @@ (let val subst = unify schemeT T in - if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg))) + if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS thy))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta]) - end handle TUNIFY => default_tr' sg tm) + end handle TUNIFY => default_tr' context tm) else raise Match (* give print translation of specialised record a chance *) | _ => raise Match) - else default_tr' sg tm + else default_tr' context tm end -fun record_type_tr' sep mark record record_scheme sg t = +fun record_type_tr' sep mark record record_scheme context t = let - fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg); + val thy = Context.theory_of context; + fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); - val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t) + val T = Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t) - fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T); + fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T); fun field_lst T = (case T of Type (ext,args) => (case try (unsuffix ext_typeN) ext of SOME ext' - => (case get_extfields sg ext' of + => (case get_extfields thy ext' of SOME flds - => (case get_fieldext sg (fst (hd flds)) of + => (case get_fieldext thy (fst (hd flds)) of SOME (_,alphas) => (let val (f::fs) = but_last flds; - val flds' = apfst (Sign.extern_const sg) f + val flds' = apfst (Sign.extern_const thy) f ::map (apfst NameSpace.base) fs; val (args',more) = split_last args; val alphavars = map Type.varifyT (but_last alphas); - val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args') + val (subst,_)= fold (Sign.typ_unify thy) (alphavars~~args') (Vartab.empty,0); val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT)) flds'; @@ -778,8 +783,8 @@ fun gen_record_type_tr' name = let val name_sfx = suffix ext_typeN name; - fun tr' sg ts = record_type_tr' "_field_types" "_field_type" - "_record_type" "_record_type_scheme" sg + fun tr' context ts = record_type_tr' "_field_types" "_field_type" + "_record_type" "_record_type_scheme" context (list_comb (Syntax.const name_sfx,ts)) in (name_sfx,tr') end @@ -789,8 +794,9 @@ let val name_sfx = suffix ext_typeN name; val default_tr' = record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme" - fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg - (list_comb (Syntax.const name_sfx,ts)) + fun tr' context ts = + record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context + (list_comb (Syntax.const name_sfx,ts)) in (name_sfx, tr') end; (** record simprocs **) @@ -798,13 +804,13 @@ val record_quick_and_dirty_sensitive = ref false; -fun quick_and_dirty_prove stndrd sg asms prop tac = +fun quick_and_dirty_prove stndrd thy asms prop tac = if !record_quick_and_dirty_sensitive andalso !quick_and_dirty - then Goal.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) + then Goal.prove thy [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) (K (SkipProof.cheat_tac HOL.thy)) (* standard can take quite a while for large records, thats why * we varify the proposition manually here.*) - else let val prf = Goal.prove sg [] asms prop tac; + else let val prf = Goal.prove thy [] asms prop tac; in if stndrd then standard prf else prf end; fun quick_and_dirty_prf noopt opt () = @@ -813,19 +819,19 @@ else opt (); -fun prove_split_simp sg ss T prop = +fun prove_split_simp thy ss T prop = let - val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg; + val {sel_upd={simpset,...},extsplit,...} = RecordsData.get thy; val extsplits = Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms) ([],dest_recTs T); - val thms = (case get_splits sg (rec_id (~1) T) of + val thms = (case get_splits thy (rec_id (~1) T) of SOME (all_thm,_,_,_) => all_thm::(case extsplits of [thm] => [] | _ => extsplits) (* [thm] is the same as all_thm *) | NONE => extsplits) in - quick_and_dirty_prove true sg [] prop + quick_and_dirty_prove true thy [] prop (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1) end; @@ -850,13 +856,13 @@ *) val record_simproc = Simplifier.simproc HOL.thy "record_simp" ["x"] - (fn sg => fn ss => fn t => + (fn thy => fn ss => fn t => (case t of (sel as Const (s, Type (_,[domS,rangeS])))$ ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=> - if is_selector sg s then - (case get_updates sg u of SOME u_name => + if is_selector thy s then + (case get_updates thy u of SOME u_name => let - val {sel_upd={updates,...},extfields,...} = RecordsData.get sg; + val {sel_upd={updates,...},extfields,...} = RecordsData.get thy; fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) = (case Symtab.lookup updates u of @@ -890,9 +896,9 @@ (case mk_eq_terms (upd$k$r) of SOME (trm,trm',vars,update_s) => if update_s - then SOME (prove_split_simp sg ss domS + then SOME (prove_split_simp thy ss domS (list_all(vars,(equals rangeS$(sel$trm)$trm')))) - else SOME (prove_split_simp sg ss domS + else SOME (prove_split_simp thy ss domS (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm'))))) | NONE => NONE) end @@ -911,10 +917,10 @@ *) val record_upd_simproc = Simplifier.simproc HOL.thy "record_upd_simp" ["x"] - (fn sg => fn ss => fn t => + (fn thy => fn ss => fn t => (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) => let datatype ('a,'b) calc = Init of 'b | Inter of 'a - val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg; + val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy; (*fun mk_abs_var x t = (x, fastype_of t);*) fun sel_name u = NameSpace.base (unsuffix updateN u); @@ -1002,7 +1008,7 @@ in (case mk_updterm updates [] t of Inter (trm,trm',vars,_) - => SOME (prove_split_simp sg ss rT + => SOME (prove_split_simp thy ss rT (list_all(vars,(equals rT$trm$trm')))) | _ => NONE) end @@ -1024,11 +1030,11 @@ *) val record_eq_simproc = Simplifier.simproc HOL.thy "record_eq_simp" ["r = s"] - (fn sg => fn _ => fn t => + (fn thy => fn _ => fn t => (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ => (case rec_id (~1) T of "" => NONE - | name => (case get_equalities sg name of + | name => (case get_equalities thy name of NONE => NONE | SOME thm => SOME (thm RS Eq_TrueI))) | _ => NONE)); @@ -1042,7 +1048,7 @@ *) fun record_split_simproc P = Simplifier.simproc HOL.thy "record_split_simp" ["x"] - (fn sg => fn _ => fn t => + (fn thy => fn _ => fn t => (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm => if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then (case rec_id (~1) T of @@ -1050,7 +1056,7 @@ | name => let val split = P t in if split <> 0 then - (case get_splits sg (rec_id split T) of + (case get_splits thy (rec_id split T) of NONE => NONE | SOME (all_thm, All_thm, Ex_thm,_) => SOME (case quantifier of @@ -1065,15 +1071,15 @@ val record_ex_sel_eq_simproc = Simplifier.simproc HOL.thy "record_ex_sel_eq_simproc" ["Ex t"] - (fn sg => fn ss => fn t => + (fn thy => fn ss => fn t => let fun prove prop = - quick_and_dirty_prove true sg [] prop - (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset sg) + quick_and_dirty_prove true thy [] prop + (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); fun mkeq (lr,Teq,(sel,Tsel),x) i = - if is_selector sg sel then + if is_selector thy sel then let val x' = if not (loose_bvar1 (x,0)) then Free ("x" ^ string_of_int i, range_type Tsel) else raise TERM ("",[x]); @@ -1118,7 +1124,7 @@ *) fun record_split_simp_tac thms P i st = let - val sg = Thm.sign_of_thm st; + val thy = Thm.theory_of_thm st; val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => @@ -1129,9 +1135,9 @@ val frees = List.filter (is_recT o type_of) (term_frees goal); fun mk_split_free_tac free induct_thm i = - let val cfree = cterm_of sg free; + let val cfree = cterm_of thy free; val (_$(_$r)) = concl_of induct_thm; - val crec = cterm_of sg r; + val crec = cterm_of thy r; val thm = cterm_instantiate [(crec,cfree)] induct_thm; in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i, rtac thm i, @@ -1143,7 +1149,7 @@ "" => NONE | name => let val split = P free in if split <> 0 then - (case get_splits sg (rec_id split T) of + (case get_splits thy (rec_id split T) of NONE => NONE | SOME (_,_,_,induct_thm) => SOME (mk_split_free_tac free induct_thm i)) @@ -1156,7 +1162,7 @@ val simprocs = if has_rec goal then [record_split_simproc P] else []; in st |> ((EVERY split_frees_tacs) - THEN (Simplifier.full_simp_tac (get_simpset sg addsimps thms addsimprocs simprocs) i)) + THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms addsimprocs simprocs) i)) end handle Empty => Seq.empty; end; @@ -1165,7 +1171,7 @@ (* splits all records in the goal, which are quantified by ! or !!. *) fun record_split_tac i st = let - val sg = Thm.sign_of_thm st; + val thy = Thm.theory_of_thm st; val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => @@ -1257,17 +1263,17 @@ instantiates x1 ... xn with parameters x1 ... xn *) fun ex_inst_tac i st = let - val sg = sign_of_thm st; + val thy = Thm.theory_of_thm st; val g = nth (prems_of st) (i - 1); val params = Logic.strip_params g; val exI' = Thm.lift_rule (Thm.cprem_of st i) exI; val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI')); - val cx = cterm_of sg (fst (strip_comb x)); + val cx = cterm_of thy (fst (strip_comb x)); in Seq.single (Library.foldl (fn (st,v) => Seq.hd (compose_tac (false, cterm_instantiate - [(cx,cterm_of sg (list_abs (params,Bound v)))] exI',1) + [(cx,cterm_of thy (list_abs (params,Bound v)))] exI',1) i st)) (st,((length params) - 1) downto 0)) end; @@ -1427,10 +1433,9 @@ fun cases_prf_opt () = let - val sg = (sign_of defs_thy); val (_$(Pvar$_)) = concl_of induct; val ind = cterm_instantiate - [(cterm_of sg Pvar, cterm_of sg + [(cterm_of defs_thy Pvar, cterm_of defs_thy (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))] induct; in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; @@ -1459,11 +1464,10 @@ upd_conv_props; fun upd_convs_prf_opt () = let - val sg = sign_of defs_thy; fun mkrefl (c,T) = Thm.reflexive - (cterm_of sg (Free (variant variants (base c ^ "'"),T))); + (cterm_of defs_thy (Free (variant variants (base c ^ "'"),T))); val refls = map mkrefl fields_more; - val constr_refl = Thm.reflexive (cterm_of sg (head_of ext)); + val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext)); val dest_convs' = map mk_meta_eq dest_convs; fun mkthm (udef,(fld_refl,thms)) = @@ -1477,8 +1481,8 @@ val (_$(_$v$r)$_) = prop_of udef; val (_$v'$_) = prop_of fld_refl; val udef' = cterm_instantiate - [(cterm_of sg v,cterm_of sg v'), - (cterm_of sg r,cterm_of sg ext)] udef; + [(cterm_of defs_thy v,cterm_of defs_thy v'), + (cterm_of defs_thy r,cterm_of defs_thy ext)] udef; in standard (Thm.transitive udef' bdyeq) end; in map mkthm (rev upd_defs ~~ (mixit dest_convs' refls)) end; @@ -1874,10 +1878,9 @@ fun cases_scheme_prf_opt () = let - val sg = (sign_of defs_thy); val (_$(Pvar$_)) = concl_of induct_scheme; val ind = cterm_instantiate - [(cterm_of sg Pvar, cterm_of sg + [(cterm_of defs_thy Pvar, cterm_of defs_thy (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))] induct_scheme; in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; @@ -1910,14 +1913,13 @@ fun split_object_prf_opt () = let - val sg = sign_of defs_thy; - val cPI= cterm_of sg (lambda r0 (Trueprop (P$r0))); + val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P$r0))); val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard)); - val cP = cterm_of sg P; + val cP = cterm_of defs_thy P; val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard; val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); - val cl = cterm_of sg (HOLogic.mk_Trueprop l); - val cr = cterm_of sg (HOLogic.mk_Trueprop r); + val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); + val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); val thl = assume cl (*All r. P r*) (* 1 *) |> obj_to_meta_all (*!!r. P r*) |> equal_elim split_meta' (*!!n m more. P (ext n m more)*)