# HG changeset patch # User wenzelm # Date 1119298439 -7200 # Node ID 1a12cdb6ee6b7352c256c1ae4b53ff7fe8b8c025 # Parent 77ae3bfa8b76021439179437c24b7f3af2055e4e get_thm(s): Name; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Mon Jun 20 22:13:59 2005 +0200 @@ -82,9 +82,9 @@ ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^ "\nCommutative rings in proof context: " ^ commas comm_rings); val simps = - List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", NONE)) + List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules"))) non_comm_rings) @ - List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", NONE)) + List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules"))) comm_rings); in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps)) end; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Jun 20 22:13:59 2005 +0200 @@ -401,7 +401,7 @@ fun dom_rng (Type("fun",[dom,rng])) = (dom,rng) | dom_rng _ = raise ERR "dom_rng" "Not a functional type" -fun mk_thy_const thy Thy Name Ty = Const(intern_const_name Thy Name thy,Ty) +fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) local fun get_type sg thyname name = @@ -409,12 +409,12 @@ SOME ty => ty | NONE => raise ERR "get_type" (name ^ ": No such constant") in -fun prim_mk_const thy Thy Name = +fun prim_mk_const thy Thy Nam = let - val name = intern_const_name Thy Name thy + val name = intern_const_name Thy Nam thy val cmaps = HOL4ConstMaps.get thy in - case StringPair.lookup(cmaps,(Thy,Name)) of + case StringPair.lookup(cmaps,(Thy,Nam)) of SOME(_,_,SOME ty) => Const(name,ty) | _ => Const(name,get_type (sign_of thy) Thy name) end @@ -1236,10 +1236,10 @@ SOME (SOME thmname) => let val _ = message ("Looking for " ^ thmname) - val th1 = (SOME (transform_error (PureThy.get_thm thy) (thmname, NONE)) + val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname)) handle ERROR_MESSAGE _ => (case split_name thmname of - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (listname, NONE),idx-1)) + SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1)) handle _ => NONE) | NONE => NONE)) in diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Library/word_setup.ML --- a/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:59 2005 +0200 @@ -24,7 +24,7 @@ fun add_word thy = let (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**) - val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", NONE) + val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def") (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) = if num_is_usable t then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th) diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 20 22:13:59 2005 +0200 @@ -984,8 +984,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 sg (s ^ ".induct", NONE))); - val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE))); + val pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct")))); + val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct")))); val ntl = new_types l; in ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done))) diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Tools/datatype_package.ML Mon Jun 20 22:13:59 2005 +0200 @@ -339,7 +339,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 o rpair NONE) + map (get_thm Datatype_thy o Name) ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"] in (case (#distinct (datatype_info_err sg tname1)) of QuickAndDirty => SOME (Thm.invoke_oracle @@ -644,7 +644,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", NONE); + val size_thms = if no_size then [] else get_thms thy3 (Name "size"); val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 20 22:13:59 2005 +0200 @@ -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 o rpair NONE) + Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name) ["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", NONE), - get_thm thy4 ("Rep_" ^ s ^ "_inverse", NONE), - get_thm thy4 ("Rep_" ^ s, NONE))) new_type_names; + (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")), + get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")), + get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names; (*------------------------------------------------*) (* prove additional theorems: *) diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Mon Jun 20 22:13:59 2005 +0200 @@ -614,11 +614,11 @@ val sum_case_rewrites = (if Context.theory_name thy = "Datatype" then - PureThy.get_thms thy ("sum.cases", NONE) + PureThy.get_thms thy (Name "sum.cases") else (case ThyInfo.lookup_theory "Datatype" of NONE => [] - | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE))) + | SOME thy' => PureThy.get_thms thy' (Name "sum.cases"))) |> map mk_meta_eq; val (preds, ind_prems, mutual_ind_concl, factors) = diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOL/Tools/typedef_package.ML Mon Jun 20 22:13:59 2005 +0200 @@ -97,7 +97,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 (map (rpair NONE) witn_names) @ witn_thms; + val thms = PureThy.get_thmss thy (map Name witn_names) @ witn_thms; val tac = witn1_tac THEN TRY (rewrite_goals_tac (List.filter is_def thms)) THEN diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jun 20 22:13:59 2005 +0200 @@ -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", NONE)); +val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct"))); 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", NONE)); +val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def"))); in (#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def)))) handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOLCF/domain/interface.ML --- a/src/HOLCF/domain/interface.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOLCF/domain/interface.ML Mon Jun 20 22:13:59 2005 +0200 @@ -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) ^ ", NONE)"; + fun get dname name = "get_thm thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ")"; fun gen_vals dname name = "val "^ name ^ " = get_thm" ^ (if hd (rev (Symbol.explode name)) = "s" then "s" else "")^ - " thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE);"; + " thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ");"; 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 77ae3bfa8b76 -r 1a12cdb6ee6b src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/HOLCF/domain/theorems.ML Mon Jun 20 22:13:59 2005 +0200 @@ -63,7 +63,7 @@ (* ----- getting the axioms and definitions --------------------------------- *) -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) 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; @@ -352,7 +352,7 @@ (* ----- getting the composite axiom and definitions ------------------------ *) -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) 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; @@ -360,8 +360,8 @@ val ax_bisim_def = ga "bisim_def" comp_dnam; end; (* local *) -local fun gt s dn = get_thm thy (dn ^ "." ^ s, NONE); - fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in +local fun gt s dn = get_thm thy (Name (dn ^ "." ^ s)); + fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)) in val cases = map (gt "casedist" ) dnames; val con_rews = List.concat (map (gts "con_rews" ) dnames); val copy_rews = List.concat (map (gts "copy_rews") dnames); diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/Isar/find_theorems.ML Mon Jun 20 22:13:59 2005 +0200 @@ -38,7 +38,7 @@ | read_criterion _ Intro = Intro | read_criterion _ Elim = Elim | read_criterion _ Dest = Dest - | read_criterion ctxt (Simp str) = + | read_criterion ctxt (Simp str) = Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str])) | read_criterion ctxt (Pattern str) = Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str])); @@ -70,15 +70,15 @@ val sg = ProofContext.sign_of ctxt; val tsig = Sign.tsig_of sg; - val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg; + val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg; - fun matches pat = - is_nontrivial pat andalso + fun matches pat = + is_nontrivial pat andalso Pattern.matches tsig (if po then (pat,obj) else (obj,pat)) handle Pattern.MATCH => false; val match_thm = matches o extract_term o Thm.prop_of - in + in List.exists match_thm (extract_thms thm) end; @@ -93,7 +93,7 @@ (*filter that just looks for a string in the name, substring match only (no regexps are performed)*) -fun filter_name str_pat ((name, _), _) = is_substring str_pat name; +fun filter_name str_pat (thmref, _) = is_substring str_pat (PureThy.name_of_thmref thmref); (* filter intro/elim/dest rules *) @@ -121,8 +121,8 @@ hd o Logic.strip_imp_prems); val prems = Logic.prems_of_goal goal 1; in - prems |> - List.exists (fn prem => + prems |> + List.exists (fn prem => is_matching_thm extract_elim ctxt true prem thm andalso (check_thm ctxt) thm) end; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Jun 20 22:13:59 2005 +0200 @@ -115,7 +115,7 @@ Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems') in SOME (Envir.norm_term env'' (inc (ren tm2))) end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) - (sort (Int.compare o pairself fst) + (sort (int_ord o pairself fst) (Net.match_term rules (Pattern.eta_contract tm))) end; @@ -774,7 +774,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, NONE), (vs, s1, s2))) xs) thy))); + (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy))); val realizabilityP = OuterSyntax.command "realizability" @@ -789,7 +789,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 o rpair NONE)) xs) thy))); + (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy))); val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP]; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/Thy/thy_parse.ML Mon Jun 20 22:13:59 2005 +0200 @@ -523,7 +523,7 @@ (* standard sections *) -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", NONE);"; +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (PureThy.Name " ^ Library.quote ax ^ ");"; val mk_vals = cat_lines o map mk_val; fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/axclass.ML Mon Jun 20 22:13:59 2005 +0200 @@ -417,7 +417,7 @@ Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c])); fun witnesses thy names thms = - PureThy.get_thmss thy (map (rpair NONE) names) @ + PureThy.get_thmss thy (map Name names) @ thms @ List.filter is_def (map snd (axioms_of thy)); diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/goals.ML --- a/src/Pure/goals.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/goals.ML Mon Jun 20 22:13:59 2005 +0200 @@ -315,7 +315,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)); + | NONE => get thy (Name name)); val get_thm = get_thmx I PureThy.get_thm; val get_thms = get_thmx (fn x => [x]) PureThy.get_thms; diff -r 77ae3bfa8b76 -r 1a12cdb6ee6b src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Mon Jun 20 22:13:58 2005 +0200 +++ b/src/Pure/proof_general.ML Mon Jun 20 22:13:59 2005 +0200 @@ -715,7 +715,7 @@ local val topthy = Toplevel.theory_of o Toplevel.get_state - fun pthm thy name = print_thm (get_thm thy (name, NONE)) + fun pthm thy name = print_thm (get_thm thy (Name name)) fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)]) in