# HG changeset patch # User berghofe # Date 1106585988 -3600 # Node ID 1fbd4aba46e380bbe175d5d09946e84d08dd9e72 # Parent 956d6acacf8937f83aed14cfad6224e5d837130a Adapted to modified interface of PureThy.get_thm(s). diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Jan 24 17:59:48 2005 +0100 @@ -981,8 +981,8 @@ val s = post_last_dot(fst(qtn a)); fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t | param_types _ = error "malformed induct-theorem in preprocess_td"; - val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct"))); - val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct"))); + val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", None))); + val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", None))); val ntl = new_types l; in ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done))) diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOL/Tools/datatype_package.ML Mon Jan 24 17:59:48 2005 +0100 @@ -51,8 +51,8 @@ induction : thm, size : thm list, simps : thm list} - val rep_datatype : string list option -> (xstring * Args.src list) list list -> - (xstring * Args.src list) list list -> xstring * Args.src list -> theory -> theory * + val rep_datatype : string list option -> (thmref * Args.src list) list list -> + (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory * {distinct : thm list list, inject : thm list list, exhaustion : thm list, @@ -355,7 +355,7 @@ val eq_ct = cterm_of sg eq_t; val Datatype_thy = theory "Datatype"; val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] = - map (get_thm Datatype_thy) + map (get_thm Datatype_thy o rpair None) ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"] in (case (#distinct (datatype_info_sg_err sg tname1)) of QuickAndDirty => Some (Thm.invoke_oracle @@ -583,21 +583,7 @@ (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx)) (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax); - val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~ - replicate (length descr') HOLogic.typeS); - - val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) => - map (fn (_, cargs) => - let - val Ts = map (typ_of_dtyp descr' sorts) cargs; - val recs = filter (is_rec_type o fst) (cargs ~~ Ts); - - fun mk_argT (dt, T) = - binder_types T ---> nth_elem (body_index dt, rec_result_Ts); - - val argTs = Ts @ map mk_argT recs - in argTs ---> nth_elem (i, rec_result_Ts) - end) constrs) descr'); + val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used; val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; val reccomb_names = if length descr' = 1 then [big_reccomb_name] else @@ -674,7 +660,7 @@ Theory.parent_path |>>> add_and_get_axiomss "inject" new_type_names (DatatypeProp.make_injs descr sorts); - val size_thms = if no_size then [] else get_thms thy3 "size"; + val size_thms = if no_size then [] else get_thms thy3 ("size", None); val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3; diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jan 24 17:59:48 2005 +0100 @@ -57,7 +57,7 @@ val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, In0_not_In1, In1_not_In0, - Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy) + Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair None) ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", "Lim_inject", "Suml_inject", "Sumr_inject"]; @@ -261,9 +261,9 @@ (* get axioms from theory *) val newT_iso_axms = map (fn s => - (get_thm thy4 ("Abs_" ^ s ^ "_inverse"), - get_thm thy4 ("Rep_" ^ s ^ "_inverse"), - get_thm thy4 ("Rep_" ^ s))) new_type_names; + (get_thm thy4 ("Abs_" ^ s ^ "_inverse", None), + get_thm thy4 ("Rep_" ^ s ^ "_inverse", None), + get_thm thy4 ("Rep_" ^ s, None))) new_type_names; (*------------------------------------------------*) (* prove additional theorems: *) diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOL/Tools/typedef_package.ML Mon Jan 24 17:59:48 2005 +0100 @@ -101,7 +101,7 @@ fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) = let val is_def = Logic.is_equals o #prop o Thm.rep_thm; - val thms = PureThy.get_thmss thy witn_names @ witn_thms; + val thms = PureThy.get_thmss thy (map (rpair None) witn_names) @ witn_thms; val tac = witn1_tac THEN TRY (rewrite_goals_tac (filter is_def thms)) THEN diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jan 24 17:59:48 2005 +0100 @@ -98,7 +98,7 @@ fun unqualify s = implode(rev(afpl(rev(explode s)))); val q_atypstr = act_name thy atyp; val uq_atypstr = unqualify q_atypstr; -val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct")); +val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", None)); in extract_constrs thy prem handle malformed => @@ -284,7 +284,7 @@ let fun left_of (( _ $ left) $ _) = left | left_of _ = raise malformed; -val aut_def = concl_of(get_thm thy (aut_name ^ "_def")); +val aut_def = concl_of (get_thm thy (aut_name ^ "_def", None)); in (#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def)))) handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOLCF/domain/interface.ML --- a/src/HOLCF/domain/interface.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOLCF/domain/interface.ML Mon Jan 24 17:59:48 2005 +0100 @@ -12,10 +12,10 @@ (* --- generation of bindings for axioms and theorems in .thy.ML - *) - fun get dname name = "get_thm thy " ^ Library.quote (dname^"."^name); + fun get dname name = "get_thm thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None)"; fun gen_vals dname name = "val "^ name ^ " = get_thm" ^ (if hd (rev (Symbol.explode name)) = "s" then "s" else "")^ - " thy " ^ Library.quote (dname^"."^name)^";"; + " thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None);"; fun gen_vall name l = "val "^name^" = "^ mk_list l^";"; val rews = "iso_rews @ when_rews @\n\ \ con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\ diff -r 956d6acacf89 -r 1fbd4aba46e3 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/HOLCF/domain/theorems.ML Mon Jan 24 17:59:48 2005 +0100 @@ -65,7 +65,7 @@ (* ----- getting the axioms and definitions --------------------------------- *) -local fun ga s dn = get_thm thy (dn^"."^s) in +local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in val ax_abs_iso = ga "abs_iso" dname; val ax_rep_iso = ga "rep_iso" dname; val ax_when_def = ga "when_def" dname; @@ -341,7 +341,7 @@ (* ----- getting the composite axiom and definitions ------------------------ *) -local fun ga s dn = get_thm thy (dn^"."^s) in +local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in val axs_reach = map (ga "reach" ) dnames; val axs_take_def = map (ga "take_def" ) dnames; val axs_finite_def = map (ga "finite_def") dnames; @@ -349,8 +349,8 @@ val ax_bisim_def = ga "bisim_def" comp_dnam; end; (* local *) -local fun gt s dn = get_thm thy (dn^"."^s); - fun gts s dn = get_thms thy (dn^"."^s) in +local fun gt s dn = get_thm thy (dn ^ "." ^ s, None); + fun gts s dn = get_thms thy (dn ^ "." ^ s, None) in val cases = map (gt "casedist" ) dnames; val con_rews = flat (map (gts "con_rews" ) dnames); val copy_rews = flat (map (gts "copy_rews") dnames); diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/Pure/Proof/extraction.ML Mon Jan 24 17:59:48 2005 +0100 @@ -734,7 +734,7 @@ (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> (fn xs => Toplevel.theory (fn thy => add_realizers (map (fn (((a, vs), s1), s2) => - (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy))); + (PureThy.get_thm thy (a, None), (vs, s1, s2))) xs) thy))); val realizabilityP = OuterSyntax.command "realizability" @@ -749,7 +749,7 @@ val extractP = OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory - (fn thy => extract (map (apfst (PureThy.get_thm thy)) xs) thy))); + (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair None)) xs) thy))); val parsers = [realizersP, realizabilityP, typeofP, extractP]; diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/Pure/Thy/thy_parse.ML Mon Jan 24 17:59:48 2005 +0100 @@ -523,7 +523,7 @@ (* standard sections *) -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";"; +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", None);"; val mk_vals = cat_lines o map mk_val; fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/Pure/axclass.ML Mon Jan 24 17:59:48 2005 +0100 @@ -64,7 +64,7 @@ val is_def = Logic.is_equals o #prop o rep_thm; fun witnesses thy names thms = - PureThy.get_thmss thy names @ thms @ filter is_def (map snd (axioms_of thy)); + PureThy.get_thmss thy (map (rpair None) names) @ thms @ filter is_def (map snd (axioms_of thy)); diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/goals.ML --- a/src/Pure/goals.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/Pure/goals.ML Mon Jan 24 17:59:48 2005 +0100 @@ -330,7 +330,7 @@ fun get_thmx f get thy name = (case get_first (get_thm_locale name) (get_scope thy) of Some thm => f thm - | None => get thy name); + | None => get thy (name, None)); val get_thm = get_thmx I PureThy.get_thm; val get_thms = get_thmx (fn x => [x]) PureThy.get_thms; diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Mon Jan 24 17:56:18 2005 +0100 +++ b/src/Pure/proof_general.ML Mon Jan 24 17:59:48 2005 +0100 @@ -685,7 +685,7 @@ local val topthy = Toplevel.theory_of o Toplevel.get_state - val pthm = print_thm oo get_thm + fun pthm thy name = print_thm (get_thm thy (name, None)) fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)]) in