# HG changeset patch
# User wenzelm
# Date 1205962077 -3600
# Node ID a0e2b706ce7385a3efeeb15a3a9e723f703bfd1a
# Parent  961bbcc9d85b654c9c875758a937b85a09b4071c
renamed datatype thmref to Facts.ref, tuned interfaces;

diff -r 961bbcc9d85b -r a0e2b706ce73 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Wed Mar 19 22:27:57 2008 +0100
@@ -19,7 +19,7 @@
 ML {*
   fun check_thm name = let
     val thy = the_context ();
-    val thm = get_thm thy (Name name);
+    val thm = get_thm thy (Facts.Named (name, NONE));
     val {prop, hyps, ...} = rep_thm thm;
     val prems = Logic.strip_imp_prems prop;
     val _ = if null hyps then ()
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -1277,10 +1277,10 @@
 	case get_hol4_mapping thyname thmname thy of
 	    SOME (SOME thmname) =>
 	    let
-		val th1 = (SOME (PureThy.get_thm thy (Name thmname))
+		val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
 			   handle ERROR _ =>
 				  (case split_name thmname of
-				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
+				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
 							       handle _ => NONE)
 				     | NONE => NONE))
 	    in
@@ -2168,7 +2168,7 @@
 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
     case HOL4DefThy.get thy of
 	Replaying _ => (thy,
-          HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
+          HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
       | _ =>
 	let
             val _ = message "TYPE_INTRO:"
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -78,7 +78,7 @@
 	"SparseMatrix.sorted_sp_simps",
         "ComputeNumeral.number_norm",
 	"ComputeNumeral.natnorm"]
-    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Name n))
+    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE)))
     val ths = List.concat (map get_thms matrix_lemmas)
     val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
 in
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -977,8 +977,9 @@
 	 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 (Name (s ^ ".induct"))));		
-         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct"))));
+	 val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE));
+	 val pl = param_types (concl_of induct_rule);
+         val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule);
 	 val ntl = new_types l;
         in 
         ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -339,7 +339,7 @@
 
 fun neq_x_y ctxt x y name =
   (let
-    val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name)); 
+    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
     val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
     val tree = term_of ctree;
     val x_path = the (find_tree x tree);
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -270,7 +270,7 @@
 
     fun solve_tac ctxt (_,i) st =
       let
-        val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name);
+        val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
         val goal = List.nth (cprems_of st,i-1);
         val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
       in EVERY [rtac rule i] st
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -48,8 +48,8 @@
        split_thms : (thm * thm) list,
        induction : thm,
        simps : thm list} * theory
-  val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
-    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
+  val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list ->
+    (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory ->
       {distinct : thm list list,
        inject : thm list list,
        exhaustion : thm list,
@@ -391,7 +391,7 @@
   | ManyConstrs (thm, simpset) =>
       let
         val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
-          map (get_thm (ThyInfo.the_theory "Datatype" thy) o Name)
+          map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
             ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
       in
         Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -57,7 +57,8 @@
 
     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 Name)
+         Lim_inject, Suml_inject, Sumr_inject] =
+          map (fn a => get_thm Datatype_thy (Facts.Named (a, 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"];
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -45,7 +45,7 @@
       local_theory -> inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->
-    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
   val add_inductive_global: string ->
     {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
@@ -76,7 +76,7 @@
   val gen_add_inductive: add_ind_def ->
     bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->
-    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def ->
     bool -> OuterParse.token list ->
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -276,8 +276,7 @@
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let
     val qualifier = NameSpace.qualifier (name_of_thm induct);
-    val inducts = PureThy.get_thms thy (Name
-      (NameSpace.qualified qualifier "inducts"));
+    val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
     val iTs = term_tvars (prop_of (hd intrs));
     val ar = length vs + length iTs;
     val params = InductivePackage.params_of raw_induct;
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -18,7 +18,7 @@
       local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->
-    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> InductivePackage.inductive_result * local_theory
   val setup: theory -> theory
 end;
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -22,7 +22,7 @@
       * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
     theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
+  val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
     -> theory -> theory * {induct_rules: thm}
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Mar 19 22:27:57 2008 +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 (Name (uq_atypstr ^ ".induct")));
+val prem = prems_of (PureThy.get_thm thy (Facts.Named (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 (Name (aut_name ^ "_def")));
+val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE)));
 in
 (#T(rep_cterm(cterm_of thy (left_of aut_def))))
 handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -126,7 +126,7 @@
 (* ----- getting the axioms and definitions --------------------------------- *)
 
 local
-  fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
 in
   val ax_abs_iso  = ga "abs_iso"  dname;
   val ax_rep_iso  = ga "rep_iso"  dname;
@@ -142,7 +142,7 @@
       fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
       fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
     in
-      List.concat (map defs_of_con cons)
+      maps defs_of_con cons
     end;
   val ax_copy_def = ga "copy_def" dname;
 end; (* local *)
@@ -281,7 +281,7 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_dis_def goal tacs end;
 
-  val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
+  val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
 
   fun dis_defin (con, args) =
     let
@@ -320,7 +320,7 @@
     in pg axs_mat_def goal tacs end;
 
   val mat_apps =
-    List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
+    maps (fn (c,_) => map (one_mat c) cons) cons;
 in
   val mat_rews = mat_stricts @ mat_apps;
 end;
@@ -352,7 +352,7 @@
     in pg axs goal tacs end;
 
   val pat_stricts = map pat_strict cons;
-  val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
+  val pat_apps = maps (fn c => map (pat_app c) cons) cons;
 in
   val pat_rews = pat_stricts @ pat_apps;
 end;
@@ -379,7 +379,7 @@
         asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
     in pg [] goal tacs end;
 in
-  val con_stricts = List.concat (map con_strict cons);
+  val con_stricts = maps con_strict cons;
   val con_defins = map con_defin cons;
   val con_rews = con_stricts @ con_defins;
 end;
@@ -407,7 +407,7 @@
   fun sel_strict (_, args) =
     List.mapPartial (Option.map one_sel o sel_of) args;
 in
-  val sel_stricts = List.concat (map sel_strict cons);
+  val sel_stricts = maps sel_strict cons;
 end;
 
 local
@@ -442,9 +442,9 @@
   fun one_sel c n sel = map (sel_app c n sel) cons;
   fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
   fun one_con (c, args) =
-    List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
+    flat (map_filter I (mapn (one_sel' c) 0 args));
 in
-  val sel_apps = List.concat (map one_con cons);
+  val sel_apps = maps one_con cons;
 end;
 
 local
@@ -491,7 +491,7 @@
     fun distincts []      = []
       | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   in distincts cons end;
-val dist_les = List.concat (List.concat distincts_le);
+val dist_les = flat (flat distincts_le);
 val dist_eqs =
   let
     fun distinct (_,args1) ((_,args2), leqs) =
@@ -504,7 +504,7 @@
           [eq1, eq2]
       end;
     fun distincts []      = []
-      | distincts ((c,leqs)::cs) = List.concat
+      | distincts ((c,leqs)::cs) = flat
 	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
 		    distincts cs;
   in map standard (distincts (cons ~~ distincts_le)) end;
@@ -612,7 +612,7 @@
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
 local
-  fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
 in
   val axs_reach      = map (ga "reach"     ) dnames;
   val axs_take_def   = map (ga "take_def"  ) dnames;
@@ -622,12 +622,12 @@
 end;
 
 local
-  fun gt  s dn = get_thm  thy (Name (dn ^ "." ^ s));
-  fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
+  fun gt  s dn = PureThy.get_thm  thy (Facts.Named (dn ^ "." ^ s, NONE));
+  fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
 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);
+  val con_rews  = maps (gts "con_rews" ) dnames;
+  val copy_rews = maps (gts "copy_rews") dnames;
 end;
 
 fun dc_take dn = %%:(dn^"_take");
@@ -668,7 +668,7 @@
           val rhs = con_app2 con (app_rec_arg mk_take) args;
         in Library.foldr mk_all (map vname args, lhs === rhs) end;
       fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
-      val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
+      val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
       val simps = List.filter (has_fewer_prems 1) copy_rews;
       fun con_tac (con, args) =
         if nonlazy_rec args = []
@@ -682,7 +682,7 @@
         simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
         TRY (safe_tac HOL_cs) ::
-        List.concat (map eq_tacs eqs);
+        maps eq_tacs eqs;
     in pg copy_take_defs goal tacs end;
 in
   val take_rews = map standard
@@ -709,14 +709,14 @@
     (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
 
   fun ind_prems_tac prems = EVERY
-    (List.concat (map (fn cons =>
+    (maps (fn cons =>
       (resolve_tac prems 1 ::
-        List.concat (map (fn (_,args) => 
+        maps (fn (_,args) => 
           resolve_tac prems 1 ::
           map (K(atac 1)) (nonlazy args) @
           map (K(atac 1)) (List.filter is_rec args))
-        cons)))
-      conss));
+        cons))
+      conss);
   local 
     (* check whether every/exists constructor of the n-th part of the equation:
        it has a possibly indirectly recursive argument that isn't/is possibly 
@@ -765,9 +765,9 @@
           fun cases_tacs (cons, cases) =
             res_inst_tac [("x","x")] cases 1 ::
             asm_simp_tac (take_ss addsimps prems) 1 ::
-            List.concat (map con_tacs cons);
+            maps con_tacs cons;
         in
-          tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
+          tacs1 @ maps cases_tacs (conss ~~ cases)
         end;
     in pg'' thy [] goal tacf end;
 
@@ -836,19 +836,19 @@
               asm_simp_tac take_ss 1];
             fun con_tacs (con, args) =
               asm_simp_tac take_ss 1 ::
-              List.concat (map arg_tacs (nonlazy_rec args));
+              maps arg_tacs (nonlazy_rec args);
             fun foo_tacs n (cons, cases) =
               simp_tac take_ss 1 ::
               rtac allI 1 ::
               res_inst_tac [("x",x_name n)] cases 1 ::
               asm_simp_tac take_ss 1 ::
-              List.concat (map con_tacs cons);
+              maps con_tacs cons;
             val tacs =
               rtac allI 1 ::
               induct_tac "n" 1 ::
               simp_tac take_ss 1 ::
               TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
-              List.concat (mapn foo_tacs 1 (conss ~~ cases));
+              flat (mapn foo_tacs 1 (conss ~~ cases));
           in pg [] goal tacs end;
 
         fun one_finite (dn, l1b) =
@@ -876,7 +876,7 @@
                   ind_prems_tac prems];
               in
                 TRY (safe_tac HOL_cs) ::
-                List.concat (map finite_tacs (finites ~~ atomize finite_ind))
+                maps finite_tacs (finites ~~ atomize finite_ind)
               end;
           in pg'' thy [] (ind_term concf) tacf end;
       in (finites, ind) end (* let *)
@@ -941,7 +941,7 @@
         induct_tac "n" 1,
         simp_tac take_ss 1,
         safe_tac HOL_cs] @
-        List.concat (mapn x_tacs 0 xs);
+        flat (mapn x_tacs 0 xs);
     in pg [ax_bisim_def] goal tacs end;
 in
   val coind = 
@@ -954,11 +954,11 @@
             mk_trp (foldr1 mk_conj (map mk_eqn xs)));
       val tacs =
         TRY (safe_tac HOL_cs) ::
-        List.concat (map (fn take_lemma => [
+        maps (fn take_lemma => [
           rtac take_lemma 1,
           cut_facts_tac [coind_lemma] 1,
           fast_tac HOL_cs 1])
-        take_lemmas);
+        take_lemmas;
     in pg [] goal tacs end;
 end; (* local *)
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -267,7 +267,7 @@
     val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
     val cname = case chead_of t of Const(c,_) => c | _ =>
               fixrec_err "function is not declared as constant in theory";
-    val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
+    val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
     val simp = Goal.prove_global thy [] [] eq
           (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   in simp end;
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/args.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -82,7 +82,7 @@
   val tyname: Context.generic * T list -> string * (Context.generic * T list)
   val const: Context.generic * T list -> string * (Context.generic * T list)
   val const_proper: Context.generic * T list -> string * (Context.generic * T list)
-  val thm_sel: T list -> PureThy.interval list * T list
+  val thm_sel: T list -> Facts.interval list * T list
   val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
   val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
     -> ((int -> tactic) -> tactic) * ('a * T list)
@@ -344,9 +344,9 @@
 (* misc *)
 
 val thm_sel = parens (list1
- (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
-  nat --| $$$ "-" >> PureThy.From ||
-  nat >> PureThy.Single));
+ (nat --| $$$ "-" -- nat >> Facts.FromTo ||
+  nat --| $$$ "-" >> Facts.From ||
+  nat >> Facts.Single));
 
 val bang_facts = Scan.peek (fn context =>
   $$$ "!" >> (fn _ => (warning "use of prems in proof method";
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -19,7 +19,7 @@
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
-  val eval_thms: Proof.context -> (thmref * src list) list -> thm list
+  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val map_specs: ('a -> 'att) ->
     (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
   val map_facts: ('a -> 'att) ->
@@ -157,34 +157,36 @@
 
 local
 
-val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
-
 val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
 
-fun gen_thm pick = Scan.depend (fn st =>
-  Args.$$$ "[" |-- Args.attribs (intern (Context.theory_of st)) --| Args.$$$ "]"
-    >> (fn srcs =>
+fun gen_thm pick = Scan.depend (fn context =>
+  let
+    val thy = Context.theory_of context;
+    val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
+    fun get_fact s = get (Facts.Fact s);
+    fun get_named s = get (Facts.Named (s, NONE));
+  in
+    Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
       let
-        val atts = map (attribute_i (Context.theory_of st)) srcs;
-        val (st', th') = Library.apply atts (st, Drule.dummy_thm);
-      in (st', pick "" [th']) end) ||
-  (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
-    >> (fn (s, fact) => ("", Fact s, fact)) ||
-  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
-    >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
-  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name)
-    >> (fn (name, fact) => (name, Name name, fact)))
-  -- Args.opt_attribs (intern (Context.theory_of st))
-  >> (fn ((name, thmref, fact), srcs) =>
-    let
-      val ths = PureThy.select_thm thmref fact;
-      val atts = map (attribute_i (Context.theory_of st)) srcs;
-      val (st', ths') = foldl_map (Library.apply atts) (st, ths);
-    in (st', pick name ths') end));
+        val atts = map (attribute_i thy) srcs;
+        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
+      in (context', pick "" [th']) end)
+    ||
+    (Scan.ahead Args.alt_name -- Args.named_fact get_fact
+      >> (fn (s, fact) => ("", Facts.Fact s, fact))
+    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
+      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
+    -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
+      let
+        val ths = Facts.select thmref fact;
+        val atts = map (attribute_i thy) srcs;
+        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
+      in (context', pick name ths') end)
+  end);
 
 in
 
-val thm = gen_thm PureThy.single_thm;
+val thm = gen_thm Facts.the_single;
 val multi_thm = gen_thm (K I);
 val thms = Scan.repeat multi_thm >> flat;
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -14,9 +14,9 @@
   val sym_add: attribute
   val sym_del: attribute
   val symmetric: attribute
-  val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val finally_: (thmref * Attrib.src list) list option -> bool ->
+  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/element.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -11,16 +11,16 @@
   datatype ('typ, 'term) stmt =
     Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
     Obtains of (string * ((string * 'typ option) list * 'term list)) list
-  type statement  (*= (string, string) stmt*)
-  type statement_i  (*= (typ, term) stmt*)
+  type statement = (string, string) stmt
+  type statement_i = (typ, term) stmt
   datatype ('typ, 'term, 'fact) ctxt =
     Fixes of (string * 'typ option * mixfix) list |
     Constrains of (string * 'typ) list |
     Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
     Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
     Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
-  type context (*= (string, string, thmref) ctxt*)
-  type context_i (*= (typ, term, thm list) ctxt*)
+  type context = (string, string, Facts.ref) ctxt
+  type context_i = (typ, term, thm list) ctxt
   val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
    ((string * Attrib.src list) * ('fact * Attrib.src list) list) list ->
    ((string * Attrib.src list) * ('c * Attrib.src list) list) list
@@ -99,7 +99,7 @@
   Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
   Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
 
-type context = (string, string, thmref) ctxt;
+type context = (string, string, Facts.ref) ctxt;
 type context_i = (typ, term, thm list) ctxt;
 
 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -49,7 +49,7 @@
 (** search criterion filters **)
 
 (*generated filters are to be of the form
-  input: (thmref * thm)
+  input: (Facts.ref * thm)
   output: (p:int, s:int) option, where
     NONE indicates no match
     p is the primary sorting criterion
@@ -107,7 +107,7 @@
   in match (space_explode "*" pat) str end;
 
 fun filter_name str_pat (thmref, _) =
-  if match_string str_pat (PureThy.name_of_thmref thmref)
+  if match_string str_pat (Facts.name_of_ref thmref)
   then SOME (0, 0) else NONE;
 
 
@@ -243,42 +243,36 @@
     EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
   | ord => ord) <> GREATER;
 
-in
+fun nicer (Facts.Named (x, _)) (Facts.Named (y, _)) = nicer_name x y
+  | nicer (Facts.Fact _) (Facts.Named _) = true
+  | nicer (Facts.Named _) (Facts.Fact _) = false;
 
-fun nicer (Fact _) _ = true
-  | nicer (PureThy.Name x) (PureThy.Name y) = nicer_name x y
-  | nicer (PureThy.Name _) (Fact _) = false
-  | nicer (PureThy.Name _) _ = true
-  | nicer (NameSelection (x, _)) (NameSelection (y, _)) = nicer_name x y
-  | nicer (NameSelection _) _ = false;
+fun rem_cdups xs =
+  let
+    fun rem_c rev_seen [] = rev rev_seen
+      | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
+      | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
+        if Thm.eq_thm_prop (t, t')
+        then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
+        else rem_c (x :: rev_seen) (y :: xs)
+  in rem_c [] xs end;
 
-end;
+in
 
 fun rem_thm_dups xs =
-  let
-    fun rem_cdups xs =
-      let
-        fun rem_c rev_seen [] = rev rev_seen
-          | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
-          | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
-            if Thm.eq_thm_prop (t, t')
-            then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
-            else rem_c (x :: rev_seen) (y :: xs)
-      in rem_c [] xs end;
+  xs ~~ (1 upto length xs)
+  |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+  |> rem_cdups
+  |> sort (int_ord o pairself #2)
+  |> map #1;
 
-  in
-    xs ~~ (1 upto length xs)
-    |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
-    |> rem_cdups
-    |> sort (int_ord o pairself #2)
-    |> map #1
-  end;
+end;
 
 
 (* print_theorems *)
 
 fun all_facts_of ctxt =
-  maps PureThy.selections
+  maps Facts.selections
    (Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @
     Facts.dest (ProofContext.facts_of ctxt));
 
@@ -300,7 +294,7 @@
     val thms = Library.drop (len - lim, matches);
 
     fun prt_fact (thmref, thm) =
-      ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
+      ProofContext.pretty_fact ctxt (Facts.string_of_ref thmref, [thm]);
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
      (if null thms then [Pretty.str "nothing found"]
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -17,7 +17,7 @@
   val oracle: bstring -> string -> string -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
-  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
+  val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
   val declaration: string -> local_theory -> local_theory
   val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
@@ -91,18 +91,18 @@
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
   val thy_deps: Toplevel.transition -> Toplevel.transition
-  val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
+  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     -> Toplevel.transition -> Toplevel.transition
   val unused_thms: (string list * string list option) option ->
     Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
-  val print_stmts: string list * (thmref * Attrib.src list) list
+  val print_stmts: string list * (Facts.ref * Attrib.src list) list
     -> Toplevel.transition -> Toplevel.transition
-  val print_thms: string list * (thmref * Attrib.src list) list
+  val print_thms: string list * (Facts.ref * Attrib.src list) list
     -> Toplevel.transition -> Toplevel.transition
-  val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
+  val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
     -> Toplevel.transition -> Toplevel.transition
   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -60,18 +60,18 @@
     ((string * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
-  val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
+  val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: ((string * Attrib.src list) *
-    (thmref * Attrib.src list) list) list -> state -> state
+    (Facts.ref * Attrib.src list) list) list -> state -> state
   val note_thmss_i: ((string * attribute list) *
     (thm list * attribute list) list) list -> state -> state
-  val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+  val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+  val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val using: ((thmref * Attrib.src list) list) list -> state -> state
+  val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val using_i: ((thm list * attribute list) list) list -> state -> state
-  val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
+  val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val unfolding_i: ((thm list * attribute list) list) list -> state -> state
   val invoke_case: string * string option list * Attrib.src list -> state -> state
   val invoke_case_i: string * string option list * attribute list -> state -> state
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -91,8 +91,8 @@
     -> Proof.context * (term list list * (Proof.context -> Proof.context))
   val fact_tac: thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
-  val get_thm: Proof.context -> thmref -> thm
-  val get_thms: Proof.context -> thmref -> thm list
+  val get_thm: Proof.context -> Facts.ref -> thm
+  val get_thms: Proof.context -> Facts.ref -> thm list
   val valid_thms: Proof.context -> string * thm list -> bool
   val add_path: string -> Proof.context -> Proof.context
   val no_base_names: Proof.context -> Proof.context
@@ -102,7 +102,7 @@
   val reset_naming: Proof.context -> Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val note_thmss: string ->
-    ((bstring * attribute list) * (thmref * attribute list) list) list ->
+    ((bstring * attribute list) * (Facts.ref * attribute list) list) list ->
       Proof.context -> (bstring * thm list) list * Proof.context
   val note_thmss_i: string ->
     ((bstring * attribute list) * (thm list * attribute list) list) list ->
@@ -790,7 +790,7 @@
 
 (* get_thm(s) *)
 
-fun retrieve_thms _ pick ctxt (Fact s) =
+fun retrieve_thms _ pick ctxt (Facts.Fact s) =
       let
         val prop = Syntax.read_prop (set_mode mode_default ctxt) s
           |> singleton (Variable.polymorphic ctxt);
@@ -802,17 +802,17 @@
         val thy = theory_of ctxt;
         val local_facts = facts_of ctxt;
         val space = Facts.space_of local_facts;
-        val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
-        val name = PureThy.name_of_thmref thmref;
+        val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
+        val name = Facts.name_of_ref thmref;
         val thms =
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup local_facts name of
-              SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
+              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
             | NONE => from_thy thy xthmref);
       in pick name thms end;
 
-val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
+val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
 val get_thms = retrieve_thms PureThy.get_thms (K I);
 val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
 
@@ -820,7 +820,7 @@
 (* valid_thms *)
 
 fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_thms_silent ctxt (Name name)) () of
+  (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -111,8 +111,9 @@
             if a <> "" then ((a, ths), j)
             else if m = n then ((name, ths), j)
             else if m = 1 then
-              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
-            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
+              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
+            else
+              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
           end;
       in fst (fold_map name_res res 1) end;
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -17,10 +17,10 @@
   val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
   val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
   val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
-  val xthm: token list -> (thmref * Attrib.src list) * token list
-  val xthms1: token list -> (thmref * Attrib.src list) list * token list
+  val xthm: token list -> (Facts.ref * Attrib.src list) * token list
+  val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   val name_facts: token list ->
-    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
+    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
   val locale_mixfix: token list -> mixfix * token list
   val locale_fixes: token list -> (string * string option * mixfix) list * token list
   val locale_insts: token list ->
@@ -65,13 +65,13 @@
 val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
 
 val thm_sel = P.$$$ "(" |-- P.list1
- (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
-  P.nat --| P.minus >> PureThy.From ||
-  P.nat >> PureThy.Single) --| P.$$$ ")";
+ (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
+  P.nat --| P.minus >> Facts.From ||
+  P.nat >> Facts.Single) --| P.$$$ ")";
 
 val xthm =
-  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
-  (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
+  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
+  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
 
 val xthms1 = Scan.repeat1 xthm;
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -43,10 +43,11 @@
     local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
-  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
-    -> local_theory -> (bstring * thm list) list * local_theory
-  val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-    -> local_theory -> (bstring * thm list) list * local_theory
+  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory
+  val theorems_cmd: string ->
+    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) ->
     string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -264,21 +264,21 @@
 
 (** fact references **)
 
-fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
-fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
+fun thm name = ProofContext.get_thm (the_local_context ()) (Facts.Named (name, NONE));
+fun thms name = ProofContext.get_thms (the_local_context ()) (Facts.Named (name, NONE));
 
 
 local
 
-fun print_interval (FromTo arg) =
-      "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
-  | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i
-  | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i;
+fun print_interval (Facts.FromTo arg) =
+      "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
+  | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
+  | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
 
 fun thm_sel name =
-  Args.thm_sel >> (fn is => "PureThy.NameSelection " ^
-    ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is))
-  || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name);
+  Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
+    ML_Syntax.print_pair ML_Syntax.print_string
+      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
 
 fun thm_antiq kind = value_antiq kind
   (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -766,7 +766,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 (Name a), (vs, s1, s2))) xs) thy)));
+         (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
 
 val _ =
   OuterSyntax.command "realizability"
@@ -780,8 +780,8 @@
 
 val _ =
   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 Name)) xs) thy)));
+    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+      extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
 
 val etype_of = etype_of o add_syntax;
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -712,7 +712,7 @@
                    What we want is mapping onto simple PGIP name/context model. *)
                 val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
                 val thy = Context.theory_of_proof ctx
-                val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
+                val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
                 val deps = filter_out (equal "")
                                       (Symtab.keys (fold Proofterm.thms_of_proof
                                                          (map Thm.proof_of ths) Symtab.empty))
@@ -764,7 +764,7 @@
                                         [] (* asms *)
                                         th))
 
-        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
+        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
 
         val string_of_thy = Output.output o
                                 Pretty.string_of o (ProofDisplay.pretty_full_theory false)
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/facts.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -7,6 +7,16 @@
 
 signature FACTS =
 sig
+  val the_single: string -> thm list -> thm
+  datatype interval = FromTo of int * int | From of int | Single of int
+  datatype ref =
+    Named of string * interval list option |
+    Fact of string
+  val string_of_ref: ref -> string
+  val name_of_ref: ref -> string
+  val map_name_of_ref: (string -> string) -> ref -> ref
+  val select: ref -> thm list -> thm list
+  val selections: string * thm list -> (ref * thm) list
   type T
   val space_of: T -> NameSpace.T
   val lookup: T -> string -> thm list option
@@ -24,7 +34,76 @@
 structure Facts: FACTS =
 struct
 
-(* datatype *)
+(** fact references **)
+
+fun the_single _ [th] : thm = th
+  | the_single name _ = error ("Single theorem expected " ^ quote name);
+
+
+(* datatype interval *)
+
+datatype interval =
+  FromTo of int * int |
+  From of int |
+  Single of int;
+
+fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
+  | string_of_interval (From i) = string_of_int i ^ "-"
+  | string_of_interval (Single i) = string_of_int i;
+
+fun interval n iv =
+  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
+    (case iv of
+      FromTo (i, j) => if i <= j then i upto j else err ()
+    | From i => if i <= n then i upto n else err ()
+    | Single i => [i])
+  end;
+
+
+(* datatype ref *)
+
+datatype ref =
+  Named of string * interval list option |
+  Fact of string;
+
+fun name_of_ref (Named (name, _)) = name
+  | name_of_ref (Fact _) = error "Illegal literal fact";
+
+fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
+  | map_name_of_ref _ r = r;
+
+fun string_of_ref (Named (name, NONE)) = name
+  | string_of_ref (Named (name, SOME is)) =
+      name ^ enclose "(" ")" (commas (map string_of_interval is))
+  | string_of_ref (Fact _) = error "Illegal literal fact";
+
+
+(* select *)
+
+fun select (Fact _) ths = ths
+  | select (Named (_, NONE)) ths = ths
+  | select (Named (name, SOME ivs)) ths =
+      let
+        val n = length ths;
+        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
+        fun sel i =
+          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
+          else nth ths (i - 1);
+        val is = maps (interval n) ivs handle Fail msg => err msg;
+      in map sel is end;
+
+
+(* selections *)
+
+fun selections (name, [th]) = [(Named (name, NONE), th)]
+  | selections (name, ths) =
+      map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
+
+
+
+(** fact environment **)
+
+(* datatype T *)
 
 datatype T = Facts of
  {facts: thm list NameSpace.table,
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/pure_thy.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -7,14 +7,8 @@
 
 signature BASIC_PURE_THY =
 sig
-  datatype interval = FromTo of int * int | From of int | Single of int
-  datatype thmref =
-    Name of string |
-    NameSelection of string * interval list |
-    Fact of string
-  val get_thm: theory -> thmref -> thm
-  val get_thms: theory -> thmref -> thm list
-  val get_thmss: theory -> thmref list -> thm list
+  val get_thm: theory -> Facts.ref -> thm
+  val get_thms: theory -> Facts.ref -> thm list
   structure ProtoPure:
     sig
       val thy: theory
@@ -44,13 +38,7 @@
   val kind_internal: attribute
   val has_internal: Markup.property list -> bool
   val is_internal: thm -> bool
-  val string_of_thmref: thmref -> string
-  val single_thm: string -> thm list -> thm
-  val name_of_thmref: thmref -> string
-  val map_name_of_thmref: (string -> string) -> thmref -> thmref
-  val select_thm: thmref -> thm list -> thm list
-  val selections: string * thm list -> (thmref * thm) list
-  val get_thms_silent: theory -> thmref -> thm list
+  val get_thms_silent: theory -> Facts.ref -> thm list
   val theorems_of: theory -> thm list NameSpace.table
   val all_facts_of: theory -> Facts.T
   val thms_of: theory -> (string * thm) list
@@ -73,7 +61,7 @@
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   val note: string -> string * thm -> theory -> thm * theory
   val note_thmss: string -> ((bstring * attribute list) *
-    (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   val note_thmss_i: string -> ((bstring * attribute list) *
     (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
@@ -182,75 +170,6 @@
 fun the_thms _ (SOME thms) = thms
   | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
 
-fun single_thm _ [thm] = thm
-  | single_thm name _ = error ("Single theorem expected " ^ quote name);
-
-
-(* datatype interval *)
-
-datatype interval =
-  FromTo of int * int |
-  From of int |
-  Single of int;
-
-fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
-  | string_of_interval (From i) = string_of_int i ^ "-"
-  | string_of_interval (Single i) = string_of_int i;
-
-fun interval n iv =
-  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
-    (case iv of
-      FromTo (i, j) => if i <= j then i upto j else err ()
-    | From i => if i <= n then i upto n else err ()
-    | Single i => [i])
-  end;
-
-
-(* datatype thmref *)
-
-datatype thmref =
-  Name of string |
-  NameSelection of string * interval list |
-  Fact of string;
-
-fun name_of_thmref (Name name) = name
-  | name_of_thmref (NameSelection (name, _)) = name
-  | name_of_thmref (Fact _) = error "Illegal literal fact";
-
-fun map_name_of_thmref f (Name name) = Name (f name)
-  | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
-  | map_name_of_thmref _ thmref = thmref;
-
-fun string_of_thmref (Name name) = name
-  | string_of_thmref (NameSelection (name, is)) =
-      name ^ enclose "(" ")" (commas (map string_of_interval is))
-  | string_of_thmref (Fact _) = error "Illegal literal fact";
-
-
-(* select_thm *)
-
-fun select_thm (Name _) thms = thms
-  | select_thm (Fact _) thms = thms
-  | select_thm (NameSelection (name, ivs)) thms =
-      let
-        val n = length thms;
-        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
-        fun select i =
-          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
-          else nth thms (i - 1);
-        val is = maps (interval n) ivs handle Fail msg => err msg;
-      in map select is end;
-
-
-(* selections *)
-
-fun selections (name, [thm]) = [(Name name, thm)]
-  | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
-      (NameSelection (name, [Single i]), thm));
-
-
-(* lookup/get thms *)
-
 local
 
 fun lookup_thms thy xname =
@@ -270,7 +189,7 @@
 
 fun get_fact silent theory thmref =
   let
-    val name = name_of_thmref thmref;
+    val name = Facts.name_of_ref thmref;
     val new_res = lookup_fact theory name;
     val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
     val is_same =
@@ -283,14 +202,13 @@
       else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
         show_result new_res ^ " vs " ^ show_result old_res ^
         Position.str_of (Position.thread_data ()));
-  in Option.map #2 old_res |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end;
+  in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
 
 in
 
 val get_thms_silent = get_fact true;
 val get_thms = get_fact false;
-fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
-fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
+fun get_thm thy thmref = Facts.the_single (Facts.name_of_ref thmref) (get_thms thy thmref);
 
 end;
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -192,10 +192,10 @@
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
 local
-    fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname)
+    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
     val eq_th = get_thm "HOL.eq_reflection"
 in
-  fun eq_to_meta th = (eq_th OF [th] handle _ => th)
+  fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
 end
 
 
diff -r 961bbcc9d85b -r a0e2b706ce73 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Tools/code/code_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -187,7 +187,7 @@
         val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
         val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
         val tfree_vars = map Logic.mk_type tfrees';
-        val c = PureThy.string_of_thmref thmref
+        val c = Facts.string_of_ref thmref
           |> NameSpace.explode
           |> (fn [x] => [x] | (x::xs) => xs)
           |> space_implode "_"
@@ -195,7 +195,7 @@
       in if c = "" then NONE else SOME (thmref, propdef) end;
   in
     Facts.dest (PureThy.all_facts_of thy)
-    |> maps PureThy.selections
+    |> maps Facts.selections
     |> map_filter select
     |> map_filter mk_codeprop
   end;
@@ -206,7 +206,7 @@
     fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
     fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
       let
-        val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
+        val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
           ^ " as code property " ^ quote raw_c);
         val ([raw_c'], names') = Name.variants [raw_c] names;
         val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
diff -r 961bbcc9d85b -r a0e2b706ce73 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
   val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
   val add_datatype: string * string list -> (string * string list * mixfix) list list ->
-    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
-    (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
 end;
 
 functor Add_datatype_def_Fun
diff -r 961bbcc9d85b -r a0e2b706ce73 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -13,8 +13,8 @@
   val induct_tac: string -> int -> tactic
   val exhaust_tac: string -> int -> tactic
   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
-  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
-    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
+  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
+    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -167,8 +167,8 @@
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let
     val ctxt = ProofContext.init thy;
-    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
-    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
+    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
+    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
diff -r 961bbcc9d85b -r a0e2b706ce73 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
     thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   val add_inductive: string list * string ->
     ((bstring * string) * Attrib.src list) list ->
-    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
-    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
+    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
     theory -> theory * inductive_result
 end;