simplified get_thm(s): back to plain name argument;
authorwenzelm
Thu Mar 20 00:20:44 2008 +0100 (2008-03-20)
changeset 263430dd2eab7b296
parent 26342 0f65fa163304
child 26344 04dacc6809b6
simplified get_thm(s): back to plain name argument;
src/FOL/ex/LocaleTest.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  ML {*
     1.5    fun check_thm name = let
     1.6      val thy = the_context ();
     1.7 -    val thm = get_thm thy (Facts.Named (name, NONE));
     1.8 +    val thm = PureThy.get_thm thy name;
     1.9      val {prop, hyps, ...} = rep_thm thm;
    1.10      val prems = Logic.strip_imp_prems prop;
    1.11      val _ = if null hyps then ()
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Mar 19 22:50:42 2008 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Mar 20 00:20:44 2008 +0100
     2.3 @@ -1277,10 +1277,10 @@
     2.4  	case get_hol4_mapping thyname thmname thy of
     2.5  	    SOME (SOME thmname) =>
     2.6  	    let
     2.7 -		val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
     2.8 +		val th1 = (SOME (PureThy.get_thm thy thmname)
     2.9  			   handle ERROR _ =>
    2.10  				  (case split_name thmname of
    2.11 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
    2.12 +				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
    2.13  							       handle _ => NONE)
    2.14  				     | NONE => NONE))
    2.15  	    in
    2.16 @@ -2158,17 +2158,10 @@
    2.17        add_dump ("syntax\n  "^n^" :: _ "^syn) thy
    2.18      end
    2.19  
    2.20 -(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
    2.21 -fun choose_upon_replay_history thy s dth =
    2.22 -    case Symtab.lookup (!type_intro_replay_history) s of
    2.23 -	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
    2.24 -      | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
    2.25 -*)
    2.26 -
    2.27  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
    2.28      case HOL4DefThy.get thy of
    2.29  	Replaying _ => (thy,
    2.30 -          HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
    2.31 +          HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
    2.32        | _ =>
    2.33  	let
    2.34              val _ = message "TYPE_INTRO:"
     3.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Mar 19 22:50:42 2008 +0100
     3.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Thu Mar 20 00:20:44 2008 +0100
     3.3 @@ -78,8 +78,8 @@
     3.4  	"SparseMatrix.sorted_sp_simps",
     3.5          "ComputeNumeral.number_norm",
     3.6  	"ComputeNumeral.natnorm"]
     3.7 -    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE)))
     3.8 -    val ths = List.concat (map get_thms matrix_lemmas)
     3.9 +    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n)
    3.10 +    val ths = maps get_thms matrix_lemmas
    3.11      val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
    3.12  in
    3.13  
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:50:42 2008 +0100
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Mar 20 00:20:44 2008 +0100
     4.3 @@ -977,7 +977,7 @@
     4.4  	 val s =  post_last_dot(fst(qtn a));
     4.5  	 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t)))))  = t |
     4.6  	 param_types _ = error "malformed induct-theorem in preprocess_td";	
     4.7 -	 val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE));
     4.8 +	 val induct_rule = PureThy.get_thm sg (s ^ ".induct");
     4.9  	 val pl = param_types (concl_of induct_rule);
    4.10           val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule);
    4.11  	 val ntl = new_types l;
     5.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 19 22:50:42 2008 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 20 00:20:44 2008 +0100
     5.3 @@ -232,7 +232,7 @@
     5.4          val i_type = Type(ak_name_qu,[]);
     5.5          val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
     5.6          val at_type = Logic.mk_type i_type;
     5.7 -        val simp_s = HOL_ss addsimps maps (dynamic_thms thy5)
     5.8 +        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5)
     5.9                                    ["at_def",
    5.10                                     ak_name ^ "_prm_" ^ ak_name ^ "_def",
    5.11                                     ak_name ^ "_prm_" ^ ak_name ^ ".simps",
    5.12 @@ -296,7 +296,7 @@
    5.13          val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    5.14          val pt_type = Logic.mk_type i_type1;
    5.15          val at_type = Logic.mk_type i_type2;
    5.16 -        val simp_s = HOL_ss addsimps maps (dynamic_thms thy7)
    5.17 +        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7)
    5.18                                    ["pt_def",
    5.19                                     "pt_" ^ ak_name ^ "1",
    5.20                                     "pt_" ^ ak_name ^ "2",
    5.21 @@ -343,7 +343,7 @@
    5.22                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    5.23           val fs_type = Logic.mk_type i_type1;
    5.24           val at_type = Logic.mk_type i_type2;
    5.25 -         val simp_s = HOL_ss addsimps maps (dynamic_thms thy11)
    5.26 +         val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11)
    5.27                                     ["fs_def",
    5.28                                      "fs_" ^ ak_name ^ "1"];
    5.29      
    5.30 @@ -395,8 +395,8 @@
    5.31               val at_type  = Logic.mk_type i_type1;
    5.32               val at_type' = Logic.mk_type i_type2;
    5.33               val cp_type  = Logic.mk_type i_type0;
    5.34 -             val simp_s   = HOL_basic_ss addsimps maps (dynamic_thms thy') ["cp_def"];
    5.35 -             val cp1      = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
    5.36 +             val simp_s   = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"];
    5.37 +             val cp1      = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
    5.38  
    5.39               val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
    5.40               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
    5.41 @@ -426,7 +426,7 @@
    5.42                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    5.43                   val at_type  = Logic.mk_type i_type1;
    5.44                   val at_type' = Logic.mk_type i_type2;
    5.45 -                 val simp_s = HOL_ss addsimps maps (dynamic_thms thy')
    5.46 +                 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy')
    5.47                                             ["disjoint_def",
    5.48                                              ak_name ^ "_prm_" ^ ak_name' ^ "_def",
    5.49                                              ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
    5.50 @@ -466,7 +466,7 @@
    5.51           let
    5.52             val qu_name =  Sign.full_name thy' ak_name';
    5.53             val cls_name = Sign.full_name thy' ("pt_"^ak_name);
    5.54 -           val at_inst  = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst");
    5.55 +           val at_inst  = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
    5.56  
    5.57             val proof1 = EVERY [Class.intro_classes_tac [],
    5.58                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
    5.59 @@ -474,7 +474,7 @@
    5.60                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
    5.61                                   atac 1];
    5.62             val simp_s = HOL_basic_ss addsimps 
    5.63 -                        maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
    5.64 +                        maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
    5.65             val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    5.66  
    5.67           in
    5.68 @@ -496,8 +496,8 @@
    5.69       val thy18 = fold (fn ak_name => fn thy =>
    5.70         let
    5.71            val cls_name = Sign.full_name thy ("pt_"^ak_name);
    5.72 -          val at_thm   = dynamic_thm thy ("at_"^ak_name^"_inst");
    5.73 -          val pt_inst  = dynamic_thm thy ("pt_"^ak_name^"_inst");
    5.74 +          val at_thm   = PureThy.get_thm thy ("at_"^ak_name^"_inst");
    5.75 +          val pt_inst  = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
    5.76  
    5.77            fun pt_proof thm = 
    5.78                EVERY [Class.intro_classes_tac [],
    5.79 @@ -546,11 +546,11 @@
    5.80             val proof =
    5.81                 (if ak_name = ak_name'
    5.82                  then
    5.83 -                  let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst");
    5.84 +                  let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
    5.85                    in  EVERY [Class.intro_classes_tac [],
    5.86                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    5.87                  else
    5.88 -                  let val dj_inst = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name);
    5.89 +                  let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
    5.90                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
    5.91                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    5.92          in
    5.93 @@ -568,7 +568,7 @@
    5.94         val thy24 = fold (fn ak_name => fn thy => 
    5.95          let
    5.96            val cls_name = Sign.full_name thy ("fs_"^ak_name);
    5.97 -          val fs_inst  = dynamic_thm thy ("fs_"^ak_name^"_inst");
    5.98 +          val fs_inst  = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
    5.99            fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
   5.100  
   5.101            val fs_thm_unit  = fs_unit_inst;
   5.102 @@ -613,18 +613,18 @@
   5.103                val proof =
   5.104                  (if (ak_name'=ak_name'') then 
   5.105                    (let
   5.106 -                    val pt_inst  = dynamic_thm thy'' ("pt_"^ak_name''^"_inst");
   5.107 -                    val at_inst  = dynamic_thm thy'' ("at_"^ak_name''^"_inst");
   5.108 +                    val pt_inst  = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst");
   5.109 +                    val at_inst  = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst");
   5.110                    in
   5.111                     EVERY [Class.intro_classes_tac [],
   5.112                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   5.113                    end)
   5.114                  else
   5.115                    (let
   5.116 -                     val dj_inst  = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
   5.117 +                     val dj_inst  = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
   5.118                       val simp_s = HOL_basic_ss addsimps
   5.119                                          ((dj_inst RS dj_pp_forget)::
   5.120 -                                         (maps (dynamic_thms thy'')
   5.121 +                                         (maps (PureThy.get_thms thy'')
   5.122                                             [ak_name' ^"_prm_"^ak_name^"_def",
   5.123                                              ak_name''^"_prm_"^ak_name^"_def"]));
   5.124                    in
   5.125 @@ -647,9 +647,9 @@
   5.126          fold (fn ak_name' => fn thy' =>
   5.127          let
   5.128              val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   5.129 -            val cp_inst  = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   5.130 -            val pt_inst  = dynamic_thm thy' ("pt_"^ak_name^"_inst");
   5.131 -            val at_inst  = dynamic_thm thy' ("at_"^ak_name^"_inst");
   5.132 +            val cp_inst  = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   5.133 +            val pt_inst  = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
   5.134 +            val at_inst  = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
   5.135  
   5.136              fun cp_proof thm  = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
   5.137            
   5.138 @@ -804,27 +804,27 @@
   5.139  
   5.140               
   5.141               (* list of all at_inst-theorems *)
   5.142 -             val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names
   5.143 +             val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names
   5.144               (* list of all pt_inst-theorems *)
   5.145 -             val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names
   5.146 +             val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
   5.147               (* list of all cp_inst-theorems as a collection of lists*)
   5.148               val cps = 
   5.149 -                 let fun cps_fun ak1 ak2 =  dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
   5.150 +                 let fun cps_fun ak1 ak2 =  PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
   5.151                   in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
   5.152               (* list of all cp_inst-theorems that have different atom types *)
   5.153               val cps' = 
   5.154                  let fun cps'_fun ak1 ak2 = 
   5.155 -                if ak1=ak2 then NONE else SOME (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
   5.156 +                if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
   5.157                  in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
   5.158               (* list of all dj_inst-theorems *)
   5.159               val djs = 
   5.160                 let fun djs_fun ak1 ak2 = 
   5.161 -                     if ak1=ak2 then NONE else SOME(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1))
   5.162 +                     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1))
   5.163                 in map_filter I (map_product djs_fun ak_names ak_names) end;
   5.164               (* list of all fs_inst-theorems *)
   5.165 -             val fss = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names
   5.166 +             val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
   5.167               (* list of all at_inst-theorems *)
   5.168 -             val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names
   5.169 +             val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names
   5.170  
   5.171               fun inst_pt thms = maps (fn ti => instR ti pts) thms;
   5.172               fun inst_at thms = maps (fn ti => instR ti ats) thms;
     6.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 19 22:50:42 2008 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 00:20:44 2008 +0100
     6.3 @@ -57,7 +57,7 @@
     6.4    res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
     6.5  
     6.6  fun get_dyn_thm thy name atom_name =
     6.7 -  dynamic_thm thy name handle ERROR _ =>
     6.8 +  PureThy.get_thm thy name handle ERROR _ =>
     6.9      raise ERROR ("The atom type "^atom_name^" is not defined.");
    6.10  
    6.11  (* End of function waiting to be in the library :o) *)
    6.12 @@ -146,8 +146,8 @@
    6.13      val thy = theory_of_thm thm;
    6.14      val ctx = Context.init_proof thy;
    6.15      val ss = simpset_of thy;
    6.16 -    val abs_fresh = dynamic_thms thy "abs_fresh";
    6.17 -    val fresh_perm_app = dynamic_thms thy "fresh_perm_app";
    6.18 +    val abs_fresh = PureThy.get_thms thy "abs_fresh";
    6.19 +    val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
    6.20      val ss' = ss addsimps fresh_prod::abs_fresh;
    6.21      val ss'' = ss' addsimps fresh_perm_app;
    6.22      val x = hd (tl (term_vars (prop_of exI)));
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 19 22:50:42 2008 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 00:20:44 2008 +0100
     7.3 @@ -273,19 +273,19 @@
     7.4             (NominalPackage.fresh_const U T $ u $ t)) bvars)
     7.5               (ts ~~ binder_types (fastype_of p)))) prems;
     7.6  
     7.7 -    val perm_pi_simp = dynamic_thms thy "perm_pi_simp";
     7.8 -    val pt2_atoms = map (fn aT => dynamic_thm thy
     7.9 +    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    7.10 +    val pt2_atoms = map (fn aT => PureThy.get_thm thy
    7.11        ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    7.12      val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    7.13        addsimprocs [mk_perm_bool_simproc ["Fun.id"]];
    7.14 -    val fresh_bij = dynamic_thms thy "fresh_bij";
    7.15 -    val perm_bij = dynamic_thms thy "perm_bij";
    7.16 -    val fs_atoms = map (fn aT => dynamic_thm thy
    7.17 +    val fresh_bij = PureThy.get_thms thy "fresh_bij";
    7.18 +    val perm_bij = PureThy.get_thms thy "perm_bij";
    7.19 +    val fs_atoms = map (fn aT => PureThy.get_thm thy
    7.20        ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    7.21 -    val exists_fresh' = dynamic_thms thy "exists_fresh'";
    7.22 -    val fresh_atm = dynamic_thms thy "fresh_atm";
    7.23 -    val calc_atm = dynamic_thms thy "calc_atm";
    7.24 -    val perm_fresh_fresh = dynamic_thms thy "perm_fresh_fresh";
    7.25 +    val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
    7.26 +    val fresh_atm = PureThy.get_thms thy "fresh_atm";
    7.27 +    val calc_atm = PureThy.get_thms thy "calc_atm";
    7.28 +    val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
    7.29  
    7.30      fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
    7.31        let
    7.32 @@ -604,7 +604,7 @@
    7.33             | xs => error ("No such atoms: " ^ commas xs);
    7.34           atoms)
    7.35        end;
    7.36 -    val perm_pi_simp = dynamic_thms thy "perm_pi_simp";
    7.37 +    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    7.38      val eqvt_ss = HOL_basic_ss addsimps
    7.39        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    7.40        [mk_perm_bool_simproc names];
     8.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 19 22:50:42 2008 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 00:20:44 2008 +0100
     8.3 @@ -140,8 +140,8 @@
     8.4            let
     8.5              val a' = Sign.base_name a;
     8.6              val b' = Sign.base_name b;
     8.7 -            val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
     8.8 -            val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a');
     8.9 +            val cp = PureThy.get_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
    8.10 +            val dj = PureThy.get_thm thy ("dj_" ^ b' ^ "_" ^ a');
    8.11              val dj_cp' = [cp, dj] MRS dj_cp;
    8.12              val cert = SOME o cterm_of thy
    8.13            in
    8.14 @@ -309,7 +309,7 @@
    8.15      val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
    8.16  
    8.17      val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
    8.18 -    val perm_fun_def = dynamic_thm thy2 "perm_fun_def";
    8.19 +    val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
    8.20  
    8.21      val unfolded_perm_eq_thms =
    8.22        if length descr = length new_type_names then []
    8.23 @@ -353,17 +353,17 @@
    8.24      val _ = warning "perm_append_thms";
    8.25  
    8.26      (*FIXME: these should be looked up statically*)
    8.27 -    val at_pt_inst = dynamic_thm thy2 "at_pt_inst";
    8.28 -    val pt2 = dynamic_thm thy2 "pt2";
    8.29 +    val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
    8.30 +    val pt2 = PureThy.get_thm thy2 "pt2";
    8.31  
    8.32      val perm_append_thms = List.concat (map (fn a =>
    8.33        let
    8.34          val permT = mk_permT (Type (a, []));
    8.35          val pi1 = Free ("pi1", permT);
    8.36          val pi2 = Free ("pi2", permT);
    8.37 -        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    8.38 +        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    8.39          val pt2' = pt_inst RS pt2;
    8.40 -        val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
    8.41 +        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
    8.42        in List.take (map standard (split_conj_thm
    8.43          (Goal.prove_global thy2 [] []
    8.44               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    8.45 @@ -385,8 +385,8 @@
    8.46  
    8.47      val _ = warning "perm_eq_thms";
    8.48  
    8.49 -    val pt3 = dynamic_thm thy2 "pt3";
    8.50 -    val pt3_rev = dynamic_thm thy2 "pt3_rev";
    8.51 +    val pt3 = PureThy.get_thm thy2 "pt3";
    8.52 +    val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
    8.53  
    8.54      val perm_eq_thms = List.concat (map (fn a =>
    8.55        let
    8.56 @@ -394,11 +394,11 @@
    8.57          val pi1 = Free ("pi1", permT);
    8.58          val pi2 = Free ("pi2", permT);
    8.59          (*FIXME: not robust - better access these theorems using NominalData?*)
    8.60 -        val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
    8.61 -        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    8.62 +        val at_inst = PureThy.get_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
    8.63 +        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    8.64          val pt3' = pt_inst RS pt3;
    8.65          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    8.66 -        val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
    8.67 +        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
    8.68        in List.take (map standard (split_conj_thm
    8.69          (Goal.prove_global thy2 [] [] (Logic.mk_implies
    8.70               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    8.71 @@ -419,11 +419,11 @@
    8.72  
    8.73      (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
    8.74  
    8.75 -    val cp1 = dynamic_thm thy2 "cp1";
    8.76 -    val dj_cp = dynamic_thm thy2 "dj_cp";
    8.77 -    val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose";
    8.78 -    val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev";
    8.79 -    val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget";
    8.80 +    val cp1 = PureThy.get_thm thy2 "cp1";
    8.81 +    val dj_cp = PureThy.get_thm thy2 "dj_cp";
    8.82 +    val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
    8.83 +    val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
    8.84 +    val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
    8.85  
    8.86      fun composition_instance name1 name2 thy =
    8.87        let
    8.88 @@ -435,15 +435,15 @@
    8.89          val augment = map_type_tfree
    8.90            (fn (x, S) => TFree (x, cp_class :: S));
    8.91          val Ts = map (augment o body_type) perm_types;
    8.92 -        val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
    8.93 +        val cp_inst = PureThy.get_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
    8.94          val simps = simpset_of thy addsimps (perm_fun_def ::
    8.95            (if name1 <> name2 then
    8.96 -             let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
    8.97 +             let val dj = PureThy.get_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
    8.98               in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
    8.99             else
   8.100               let
   8.101 -               val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst");
   8.102 -               val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst");
   8.103 +               val at_inst = PureThy.get_thm thy ("at_" ^ name1' ^ "_inst");
   8.104 +               val pt_inst = PureThy.get_thm thy ("pt_" ^ name1' ^ "_inst");
   8.105               in
   8.106                 [cp_inst RS cp1 RS sym,
   8.107                  at_inst RS (pt_inst RS pt_perm_compose) RS sym,
   8.108 @@ -571,7 +571,7 @@
   8.109  
   8.110      val _ = warning "proving closure under permutation...";
   8.111  
   8.112 -    val abs_perm = dynamic_thms thy4 "abs_perm";
   8.113 +    val abs_perm = PureThy.get_thms thy4 "abs_perm";
   8.114  
   8.115      val perm_indnames' = List.mapPartial
   8.116        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   8.117 @@ -656,7 +656,7 @@
   8.118                asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
   8.119                asm_full_simp_tac (simpset_of thy addsimps
   8.120                  [Rep RS perm_closed RS Abs_inverse]) 1,
   8.121 -              asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy
   8.122 +              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
   8.123                  ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy)
   8.124          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
   8.125             new_type_names ~~ tyvars ~~ perm_closed_thms);
   8.126 @@ -670,7 +670,7 @@
   8.127        let
   8.128          val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
   8.129          val class = Sign.intern_class thy name;
   8.130 -        val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1
   8.131 +        val cp1' = PureThy.get_thm thy (name ^ "_inst") RS cp1
   8.132        in fold (fn ((((((Abs_inverse, Rep),
   8.133          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
   8.134            AxClass.prove_arity
   8.135 @@ -920,8 +920,8 @@
   8.136      (** prove injectivity of constructors **)
   8.137  
   8.138      val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
   8.139 -    val alpha = dynamic_thms thy8 "alpha";
   8.140 -    val abs_fresh = dynamic_thms thy8 "abs_fresh";
   8.141 +    val alpha = PureThy.get_thms thy8 "alpha";
   8.142 +    val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
   8.143  
   8.144      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   8.145        let val T = nth_dtyp' i
   8.146 @@ -1066,8 +1066,8 @@
   8.147  
   8.148      val indnames = DatatypeProp.make_tnames recTs;
   8.149  
   8.150 -    val abs_supp = dynamic_thms thy8 "abs_supp";
   8.151 -    val supp_atm = dynamic_thms thy8 "supp_atm";
   8.152 +    val abs_supp = PureThy.get_thms thy8 "abs_supp";
   8.153 +    val supp_atm = PureThy.get_thms thy8 "supp_atm";
   8.154  
   8.155      val finite_supp_thms = map (fn atom =>
   8.156        let val atomT = Type (atom, [])
   8.157 @@ -1080,7 +1080,7 @@
   8.158             (fn _ => indtac dt_induct indnames 1 THEN
   8.159              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
   8.160                (abs_supp @ supp_atm @
   8.161 -               dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
   8.162 +               PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
   8.163                 List.concat supp_thms))))),
   8.164           length new_type_names))
   8.165        end) atoms;
   8.166 @@ -1207,23 +1207,23 @@
   8.167          (descr'' ~~ recTs ~~ tnames)));
   8.168  
   8.169      val fin_set_supp = map (fn Type (s, _) =>
   8.170 -      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   8.171 +      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   8.172          at_fin_set_supp) dt_atomTs;
   8.173      val fin_set_fresh = map (fn Type (s, _) =>
   8.174 -      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   8.175 +      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   8.176          at_fin_set_fresh) dt_atomTs;
   8.177      val pt1_atoms = map (fn Type (s, _) =>
   8.178 -      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
   8.179 +      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
   8.180      val pt2_atoms = map (fn Type (s, _) =>
   8.181 -      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
   8.182 -    val exists_fresh' = dynamic_thms thy9 "exists_fresh'";
   8.183 -    val fs_atoms = dynamic_thms thy9 "fin_supp";
   8.184 -    val abs_supp = dynamic_thms thy9 "abs_supp";
   8.185 -    val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh";
   8.186 -    val calc_atm = dynamic_thms thy9 "calc_atm";
   8.187 -    val fresh_atm = dynamic_thms thy9 "fresh_atm";
   8.188 -    val fresh_left = dynamic_thms thy9 "fresh_left";
   8.189 -    val perm_swap = dynamic_thms thy9 "perm_swap";
   8.190 +      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
   8.191 +    val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
   8.192 +    val fs_atoms = PureThy.get_thms thy9 "fin_supp";
   8.193 +    val abs_supp = PureThy.get_thms thy9 "abs_supp";
   8.194 +    val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
   8.195 +    val calc_atm = PureThy.get_thms thy9 "calc_atm";
   8.196 +    val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
   8.197 +    val fresh_left = PureThy.get_thms thy9 "fresh_left";
   8.198 +    val perm_swap = PureThy.get_thms thy9 "perm_swap";
   8.199  
   8.200      fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
   8.201        let
   8.202 @@ -1496,8 +1496,8 @@
   8.203  
   8.204      (** equivariance **)
   8.205  
   8.206 -    val fresh_bij = dynamic_thms thy11 "fresh_bij";
   8.207 -    val perm_bij = dynamic_thms thy11 "perm_bij";
   8.208 +    val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
   8.209 +    val perm_bij = PureThy.get_thms thy11 "perm_bij";
   8.210  
   8.211      val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
   8.212        let
   8.213 @@ -1535,7 +1535,7 @@
   8.214      val rec_fin_supp_thms = map (fn aT =>
   8.215        let
   8.216          val name = Sign.base_name (fst (dest_Type aT));
   8.217 -        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
   8.218 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   8.219          val aset = HOLogic.mk_setT aT;
   8.220          val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
   8.221          val fins = map (fn (f, T) => HOLogic.mk_Trueprop
   8.222 @@ -1568,7 +1568,7 @@
   8.223      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
   8.224        let
   8.225          val name = Sign.base_name (fst (dest_Type aT));
   8.226 -        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
   8.227 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   8.228          val a = Free ("a", aT);
   8.229          val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
   8.230            (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
     9.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 19 22:50:42 2008 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 00:20:44 2008 +0100
     9.3 @@ -71,8 +71,8 @@
     9.4  val supports_fresh_rule = @{thm "supports_fresh"};
     9.5  
     9.6  (* pulls out dynamically a thm via the proof state *)
     9.7 -fun global_thms st name = PureThy.get_thms (theory_of_thm st) (Facts.Named (name, NONE));
     9.8 -fun global_thm  st name = PureThy.get_thm  (theory_of_thm st) (Facts.Named (name, NONE));
     9.9 +fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name;
    9.10 +fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) name;
    9.11  
    9.12  
    9.13  (* needed in the process of fully simplifying permutations *)
    9.14 @@ -111,8 +111,8 @@
    9.15              (if (applicable_app f) then
    9.16                let
    9.17                  val name = Sign.base_name n
    9.18 -                val at_inst = dynamic_thm sg ("at_" ^ name ^ "_inst")
    9.19 -                val pt_inst = dynamic_thm sg ("pt_" ^ name ^ "_inst")
    9.20 +                val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
    9.21 +                val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
    9.22                in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
    9.23              else NONE)
    9.24        | _ => NONE
    9.25 @@ -146,7 +146,7 @@
    9.26      ("general simplification of permutations", fn st =>
    9.27      let
    9.28         val ss' = Simplifier.theory_context (theory_of_thm st) ss
    9.29 -         addsimps ((List.concat (map (global_thms st) dyn_thms))@eqvt_thms)
    9.30 +         addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
    9.31           delcongs weak_congs
    9.32           addcongs strong_congs
    9.33           addsimprocs [perm_simproc_fun, perm_simproc_app]
    9.34 @@ -198,13 +198,13 @@
    9.35            SOME (Drule.instantiate'
    9.36              [SOME (ctyp_of sg (fastype_of t))]
    9.37              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
    9.38 -            (mk_meta_eq ([dynamic_thm sg ("pt_"^tname'^"_inst"),
    9.39 -             dynamic_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
    9.40 +            (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"),
    9.41 +             PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
    9.42          else
    9.43            SOME (Drule.instantiate'
    9.44              [SOME (ctyp_of sg (fastype_of t))]
    9.45              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
    9.46 -            (mk_meta_eq (dynamic_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
    9.47 +            (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
    9.48               cp1_aux)))
    9.49        else NONE
    9.50      end
    9.51 @@ -307,7 +307,7 @@
    9.52                Logic.strip_assums_concl (hd (prems_of supports_rule'));
    9.53              val supports_rule'' = Drule.cterm_instantiate
    9.54                [(cert (head_of S), cert s')] supports_rule'
    9.55 -            val fin_supp = global_thms st ("fin_supp")
    9.56 +            val fin_supp = dynamic_thms st ("fin_supp")
    9.57              val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    9.58            in
    9.59              (tactical ("guessing of the right supports-set",
    9.60 @@ -326,8 +326,8 @@
    9.61  fun fresh_guess_tac tactical ss i st =
    9.62      let 
    9.63  	val goal = List.nth(cprems_of st, i-1)
    9.64 -        val fin_supp = global_thms st ("fin_supp")
    9.65 -        val fresh_atm = global_thms st ("fresh_atm")
    9.66 +        val fin_supp = dynamic_thms st ("fin_supp")
    9.67 +        val fresh_atm = dynamic_thms st ("fresh_atm")
    9.68  	val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
    9.69          val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    9.70      in
    10.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Mar 19 22:50:42 2008 +0100
    10.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Mar 20 00:20:44 2008 +0100
    10.3 @@ -10,9 +10,6 @@
    10.4     respectively the lemma from the data-slot.
    10.5  *)
    10.6  
    10.7 -fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE));
    10.8 -fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE));
    10.9 -
   10.10  signature NOMINAL_THMDECLS =
   10.11  sig
   10.12    val print_data: Proof.context -> unit
   10.13 @@ -83,7 +80,7 @@
   10.14      let
   10.15          val mypi = Thm.cterm_of ctx (Var (pi,typi))
   10.16          val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
   10.17 -        val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
   10.18 +        val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
   10.19      in
   10.20          EVERY [tactic ("iffI applied",rtac iffI 1),
   10.21  	       tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
    11.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:50:42 2008 +0100
    11.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Mar 20 00:20:44 2008 +0100
    11.3 @@ -339,7 +339,7 @@
    11.4  
    11.5  fun neq_x_y ctxt x y name =
    11.6    (let
    11.7 -    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
    11.8 +    val dist_thm = the (try (ProofContext.get_thm ctxt) name);
    11.9      val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   11.10      val tree = term_of ctree;
   11.11      val x_path = the (find_tree x tree);
    12.1 --- a/src/HOL/Statespace/state_space.ML	Wed Mar 19 22:50:42 2008 +0100
    12.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Mar 20 00:20:44 2008 +0100
    12.3 @@ -270,7 +270,7 @@
    12.4  
    12.5      fun solve_tac ctxt (_,i) st =
    12.6        let
    12.7 -        val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
    12.8 +        val distinct_thm = ProofContext.get_thm ctxt dist_thm_name;
    12.9          val goal = List.nth (cprems_of st,i-1);
   12.10          val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
   12.11        in EVERY [rtac rule i] st
    13.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 19 22:50:42 2008 +0100
    13.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Mar 20 00:20:44 2008 +0100
    13.3 @@ -391,7 +391,7 @@
    13.4    | ManyConstrs (thm, simpset) =>
    13.5        let
    13.6          val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    13.7 -          map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
    13.8 +          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
    13.9              ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
   13.10        in
   13.11          Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    14.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 19 22:50:42 2008 +0100
    14.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 00:20:44 2008 +0100
    14.3 @@ -57,11 +57,10 @@
    14.4  
    14.5      val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
    14.6           In0_eq, In1_eq, In0_not_In1, In1_not_In0,
    14.7 -         Lim_inject, Suml_inject, Sumr_inject] =
    14.8 -          map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE)))
    14.9 -        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
   14.10 -         "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
   14.11 -         "Lim_inject", "Suml_inject", "Sumr_inject"];
   14.12 +         Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy)
   14.13 +          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
   14.14 +           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
   14.15 +           "Lim_inject", "Suml_inject", "Sumr_inject"];
   14.16  
   14.17      val descr' = List.concat descr;
   14.18  
    15.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 22:50:42 2008 +0100
    15.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 20 00:20:44 2008 +0100
    15.3 @@ -276,7 +276,7 @@
    15.4  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    15.5    let
    15.6      val qualifier = NameSpace.qualifier (name_of_thm induct);
    15.7 -    val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
    15.8 +    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
    15.9      val iTs = term_tvars (prop_of (hd intrs));
   15.10      val ar = length vs + length iTs;
   15.11      val params = InductivePackage.params_of raw_induct;
    16.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Mar 19 22:50:42 2008 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Thu Mar 20 00:20:44 2008 +0100
    16.3 @@ -98,7 +98,7 @@
    16.4  fun unqualify s = implode(rev(afpl(rev(explode s))));
    16.5  val q_atypstr = act_name thy atyp;
    16.6  val uq_atypstr = unqualify q_atypstr;
    16.7 -val prem = prems_of (PureThy.get_thm thy (Facts.Named (uq_atypstr ^ ".induct", NONE)));
    16.8 +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
    16.9  in
   16.10  extract_constrs thy prem
   16.11  handle malformed =>
   16.12 @@ -284,7 +284,7 @@
   16.13  let
   16.14  fun left_of (( _ $ left) $ _) = left |
   16.15  left_of _ = raise malformed;
   16.16 -val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE)));
   16.17 +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   16.18  in
   16.19  (#T(rep_cterm(cterm_of thy (left_of aut_def))))
   16.20  handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
    17.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:50:42 2008 +0100
    17.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Mar 20 00:20:44 2008 +0100
    17.3 @@ -126,7 +126,7 @@
    17.4  (* ----- getting the axioms and definitions --------------------------------- *)
    17.5  
    17.6  local
    17.7 -  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
    17.8 +  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
    17.9  in
   17.10    val ax_abs_iso  = ga "abs_iso"  dname;
   17.11    val ax_rep_iso  = ga "rep_iso"  dname;
   17.12 @@ -612,7 +612,7 @@
   17.13  (* ----- getting the composite axiom and definitions ------------------------ *)
   17.14  
   17.15  local
   17.16 -  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
   17.17 +  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
   17.18  in
   17.19    val axs_reach      = map (ga "reach"     ) dnames;
   17.20    val axs_take_def   = map (ga "take_def"  ) dnames;
   17.21 @@ -622,8 +622,8 @@
   17.22  end;
   17.23  
   17.24  local
   17.25 -  fun gt  s dn = PureThy.get_thm  thy (Facts.Named (dn ^ "." ^ s, NONE));
   17.26 -  fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
   17.27 +  fun gt  s dn = PureThy.get_thm  thy (dn ^ "." ^ s);
   17.28 +  fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
   17.29  in
   17.30    val cases = map (gt  "casedist" ) dnames;
   17.31    val con_rews  = maps (gts "con_rews" ) dnames;
    18.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 22:50:42 2008 +0100
    18.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 20 00:20:44 2008 +0100
    18.3 @@ -267,7 +267,7 @@
    18.4      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
    18.5      val cname = case chead_of t of Const(c,_) => c | _ =>
    18.6                fixrec_err "function is not declared as constant in theory";
    18.7 -    val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
    18.8 +    val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
    18.9      val simp = Goal.prove_global thy [] [] eq
   18.10            (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   18.11    in simp end;
    19.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 19 22:50:42 2008 +0100
    19.2 +++ b/src/Pure/Proof/extraction.ML	Thu Mar 20 00:20:44 2008 +0100
    19.3 @@ -765,8 +765,7 @@
    19.4    K.thy_decl
    19.5      (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
    19.6       (fn xs => Toplevel.theory (fn thy => add_realizers
    19.7 -       (map (fn (((a, vs), s1), s2) =>
    19.8 -         (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
    19.9 +       (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
   19.10  
   19.11  val _ =
   19.12    OuterSyntax.command "realizability"
   19.13 @@ -781,7 +780,7 @@
   19.14  val _ =
   19.15    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   19.16      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   19.17 -      extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
   19.18 +      extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
   19.19  
   19.20  val etype_of = etype_of o add_syntax;
   19.21  
    20.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 22:50:42 2008 +0100
    20.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 20 00:20:44 2008 +0100
    20.3 @@ -712,7 +712,7 @@
    20.4                     What we want is mapping onto simple PGIP name/context model. *)
    20.5                  val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
    20.6                  val thy = Context.theory_of_proof ctx
    20.7 -                val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
    20.8 +                val ths = [PureThy.get_thm thy thmname]
    20.9                  val deps = filter_out (equal "")
   20.10                                        (Symtab.keys (fold Proofterm.thms_of_proof
   20.11                                                           (map Thm.proof_of ths) Symtab.empty))
   20.12 @@ -764,7 +764,7 @@
   20.13                                          [] (* asms *)
   20.14                                          th))
   20.15  
   20.16 -        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
   20.17 +        fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
   20.18  
   20.19          val string_of_thy = Output.output o
   20.20                                  Pretty.string_of o (ProofDisplay.pretty_full_theory false)
    21.1 --- a/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 22:50:42 2008 +0100
    21.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Thu Mar 20 00:20:44 2008 +0100
    21.3 @@ -192,7 +192,7 @@
    21.4  fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
    21.5  
    21.6  local
    21.7 -    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
    21.8 +    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
    21.9      val eq_th = get_thm "HOL.eq_reflection"
   21.10  in
   21.11    fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)