renamed datatype thmref to Facts.ref, tuned interfaces;
authorwenzelm
Wed Mar 19 22:27:57 2008 +0100 (2008-03-19 ago)
changeset 26336a0e2b706ce73
parent 26335 961bbcc9d85b
child 26337 44473c957672
renamed datatype thmref to Facts.ref, tuned interfaces;
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/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_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/recdef_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/element.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_context.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/facts.ML
src/Pure/pure_thy.ML
src/Tools/Compute_Oracle/linker.ML
src/Tools/code/code_package.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Mar 19 22:27:57 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 (Name name);
     1.8 +    val thm = get_thm thy (Facts.Named (name, NONE));
     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 18:15:25 2008 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Mar 19 22:27:57 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 (Name thmname))
     2.8 +		val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
     2.9  			   handle ERROR _ =>
    2.10  				  (case split_name thmname of
    2.11 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
    2.12 +				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
    2.13  							       handle _ => NONE)
    2.14  				     | NONE => NONE))
    2.15  	    in
    2.16 @@ -2168,7 +2168,7 @@
    2.17  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
    2.18      case HOL4DefThy.get thy of
    2.19  	Replaying _ => (thy,
    2.20 -          HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
    2.21 +          HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
    2.22        | _ =>
    2.23  	let
    2.24              val _ = message "TYPE_INTRO:"
     3.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Mar 19 18:15:25 2008 +0100
     3.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Mar 19 22:27:57 2008 +0100
     3.3 @@ -78,7 +78,7 @@
     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"} (Name n))
     3.8 +    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE)))
     3.9      val ths = List.concat (map get_thms matrix_lemmas)
    3.10      val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
    3.11  in
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 18:15:25 2008 +0100
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:27:57 2008 +0100
     4.3 @@ -977,8 +977,9 @@
     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 pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct"))));		
     4.8 -         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct"))));
     4.9 +	 val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE));
    4.10 +	 val pl = param_types (concl_of induct_rule);
    4.11 +         val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule);
    4.12  	 val ntl = new_types l;
    4.13          in 
    4.14          ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
     5.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 18:15:25 2008 +0100
     5.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:27:57 2008 +0100
     5.3 @@ -339,7 +339,7 @@
     5.4  
     5.5  fun neq_x_y ctxt x y name =
     5.6    (let
     5.7 -    val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name)); 
     5.8 +    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
     5.9      val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
    5.10      val tree = term_of ctree;
    5.11      val x_path = the (find_tree x tree);
     6.1 --- a/src/HOL/Statespace/state_space.ML	Wed Mar 19 18:15:25 2008 +0100
     6.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Mar 19 22:27:57 2008 +0100
     6.3 @@ -270,7 +270,7 @@
     6.4  
     6.5      fun solve_tac ctxt (_,i) st =
     6.6        let
     6.7 -        val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name);
     6.8 +        val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
     6.9          val goal = List.nth (cprems_of st,i-1);
    6.10          val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
    6.11        in EVERY [rtac rule i] st
     7.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 19 18:15:25 2008 +0100
     7.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 19 22:27:57 2008 +0100
     7.3 @@ -48,8 +48,8 @@
     7.4         split_thms : (thm * thm) list,
     7.5         induction : thm,
     7.6         simps : thm list} * theory
     7.7 -  val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
     7.8 -    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
     7.9 +  val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list ->
    7.10 +    (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory ->
    7.11        {distinct : thm list list,
    7.12         inject : thm list list,
    7.13         exhaustion : thm list,
    7.14 @@ -391,7 +391,7 @@
    7.15    | ManyConstrs (thm, simpset) =>
    7.16        let
    7.17          val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    7.18 -          map (get_thm (ThyInfo.the_theory "Datatype" thy) o Name)
    7.19 +          map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
    7.20              ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
    7.21        in
    7.22          Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
     8.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 19 18:15:25 2008 +0100
     8.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 19 22:27:57 2008 +0100
     8.3 @@ -57,7 +57,8 @@
     8.4  
     8.5      val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
     8.6           In0_eq, In1_eq, In0_not_In1, In1_not_In0,
     8.7 -         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name)
     8.8 +         Lim_inject, Suml_inject, Sumr_inject] =
     8.9 +          map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE)))
    8.10          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    8.11           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    8.12           "Lim_inject", "Suml_inject", "Sumr_inject"];
     9.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 19 18:15:25 2008 +0100
     9.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 19 22:27:57 2008 +0100
     9.3 @@ -45,7 +45,7 @@
     9.4        local_theory -> inductive_result * local_theory
     9.5    val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     9.6      (string * string option * mixfix) list ->
     9.7 -    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
     9.8 +    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     9.9      local_theory -> inductive_result * local_theory
    9.10    val add_inductive_global: string ->
    9.11      {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    9.12 @@ -76,7 +76,7 @@
    9.13    val gen_add_inductive: add_ind_def ->
    9.14      bool -> bool -> (string * string option * mixfix) list ->
    9.15      (string * string option * mixfix) list ->
    9.16 -    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    9.17 +    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    9.18      local_theory -> inductive_result * local_theory
    9.19    val gen_ind_decl: add_ind_def ->
    9.20      bool -> OuterParse.token list ->
    10.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 18:15:25 2008 +0100
    10.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 19 22:27:57 2008 +0100
    10.3 @@ -276,8 +276,7 @@
    10.4  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    10.5    let
    10.6      val qualifier = NameSpace.qualifier (name_of_thm induct);
    10.7 -    val inducts = PureThy.get_thms thy (Name
    10.8 -      (NameSpace.qualified qualifier "inducts"));
    10.9 +    val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
   10.10      val iTs = term_tvars (prop_of (hd intrs));
   10.11      val ar = length vs + length iTs;
   10.12      val params = InductivePackage.params_of raw_induct;
    11.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 18:15:25 2008 +0100
    11.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 22:27:57 2008 +0100
    11.3 @@ -18,7 +18,7 @@
    11.4        local_theory -> InductivePackage.inductive_result * local_theory
    11.5    val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
    11.6      (string * string option * mixfix) list ->
    11.7 -    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    11.8 +    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    11.9      local_theory -> InductivePackage.inductive_result * local_theory
   11.10    val setup: theory -> theory
   11.11  end;
    12.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Mar 19 18:15:25 2008 +0100
    12.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Mar 19 22:27:57 2008 +0100
    12.3 @@ -22,7 +22,7 @@
    12.4        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    12.5    val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
    12.6      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    12.7 -  val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
    12.8 +  val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
    12.9      -> theory -> theory * {induct_rules: thm}
   12.10    val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
   12.11      -> theory -> theory * {induct_rules: thm}
    13.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Mar 19 18:15:25 2008 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Mar 19 22:27:57 2008 +0100
    13.3 @@ -98,7 +98,7 @@
    13.4  fun unqualify s = implode(rev(afpl(rev(explode s))));
    13.5  val q_atypstr = act_name thy atyp;
    13.6  val uq_atypstr = unqualify q_atypstr;
    13.7 -val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct")));
    13.8 +val prem = prems_of (PureThy.get_thm thy (Facts.Named (uq_atypstr ^ ".induct", NONE)));
    13.9  in
   13.10  extract_constrs thy prem
   13.11  handle malformed =>
   13.12 @@ -284,7 +284,7 @@
   13.13  let
   13.14  fun left_of (( _ $ left) $ _) = left |
   13.15  left_of _ = raise malformed;
   13.16 -val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def")));
   13.17 +val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE)));
   13.18  in
   13.19  (#T(rep_cterm(cterm_of thy (left_of aut_def))))
   13.20  handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
    14.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 18:15:25 2008 +0100
    14.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:27:57 2008 +0100
    14.3 @@ -126,7 +126,7 @@
    14.4  (* ----- getting the axioms and definitions --------------------------------- *)
    14.5  
    14.6  local
    14.7 -  fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
    14.8 +  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
    14.9  in
   14.10    val ax_abs_iso  = ga "abs_iso"  dname;
   14.11    val ax_rep_iso  = ga "rep_iso"  dname;
   14.12 @@ -142,7 +142,7 @@
   14.13        fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
   14.14        fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
   14.15      in
   14.16 -      List.concat (map defs_of_con cons)
   14.17 +      maps defs_of_con cons
   14.18      end;
   14.19    val ax_copy_def = ga "copy_def" dname;
   14.20  end; (* local *)
   14.21 @@ -281,7 +281,7 @@
   14.22        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   14.23      in pg axs_dis_def goal tacs end;
   14.24  
   14.25 -  val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
   14.26 +  val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
   14.27  
   14.28    fun dis_defin (con, args) =
   14.29      let
   14.30 @@ -320,7 +320,7 @@
   14.31      in pg axs_mat_def goal tacs end;
   14.32  
   14.33    val mat_apps =
   14.34 -    List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
   14.35 +    maps (fn (c,_) => map (one_mat c) cons) cons;
   14.36  in
   14.37    val mat_rews = mat_stricts @ mat_apps;
   14.38  end;
   14.39 @@ -352,7 +352,7 @@
   14.40      in pg axs goal tacs end;
   14.41  
   14.42    val pat_stricts = map pat_strict cons;
   14.43 -  val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
   14.44 +  val pat_apps = maps (fn c => map (pat_app c) cons) cons;
   14.45  in
   14.46    val pat_rews = pat_stricts @ pat_apps;
   14.47  end;
   14.48 @@ -379,7 +379,7 @@
   14.49          asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   14.50      in pg [] goal tacs end;
   14.51  in
   14.52 -  val con_stricts = List.concat (map con_strict cons);
   14.53 +  val con_stricts = maps con_strict cons;
   14.54    val con_defins = map con_defin cons;
   14.55    val con_rews = con_stricts @ con_defins;
   14.56  end;
   14.57 @@ -407,7 +407,7 @@
   14.58    fun sel_strict (_, args) =
   14.59      List.mapPartial (Option.map one_sel o sel_of) args;
   14.60  in
   14.61 -  val sel_stricts = List.concat (map sel_strict cons);
   14.62 +  val sel_stricts = maps sel_strict cons;
   14.63  end;
   14.64  
   14.65  local
   14.66 @@ -442,9 +442,9 @@
   14.67    fun one_sel c n sel = map (sel_app c n sel) cons;
   14.68    fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
   14.69    fun one_con (c, args) =
   14.70 -    List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
   14.71 +    flat (map_filter I (mapn (one_sel' c) 0 args));
   14.72  in
   14.73 -  val sel_apps = List.concat (map one_con cons);
   14.74 +  val sel_apps = maps one_con cons;
   14.75  end;
   14.76  
   14.77  local
   14.78 @@ -491,7 +491,7 @@
   14.79      fun distincts []      = []
   14.80        | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   14.81    in distincts cons end;
   14.82 -val dist_les = List.concat (List.concat distincts_le);
   14.83 +val dist_les = flat (flat distincts_le);
   14.84  val dist_eqs =
   14.85    let
   14.86      fun distinct (_,args1) ((_,args2), leqs) =
   14.87 @@ -504,7 +504,7 @@
   14.88            [eq1, eq2]
   14.89        end;
   14.90      fun distincts []      = []
   14.91 -      | distincts ((c,leqs)::cs) = List.concat
   14.92 +      | distincts ((c,leqs)::cs) = flat
   14.93  	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   14.94  		    distincts cs;
   14.95    in map standard (distincts (cons ~~ distincts_le)) end;
   14.96 @@ -612,7 +612,7 @@
   14.97  (* ----- getting the composite axiom and definitions ------------------------ *)
   14.98  
   14.99  local
  14.100 -  fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
  14.101 +  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
  14.102  in
  14.103    val axs_reach      = map (ga "reach"     ) dnames;
  14.104    val axs_take_def   = map (ga "take_def"  ) dnames;
  14.105 @@ -622,12 +622,12 @@
  14.106  end;
  14.107  
  14.108  local
  14.109 -  fun gt  s dn = get_thm  thy (Name (dn ^ "." ^ s));
  14.110 -  fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
  14.111 +  fun gt  s dn = PureThy.get_thm  thy (Facts.Named (dn ^ "." ^ s, NONE));
  14.112 +  fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
  14.113  in
  14.114    val cases = map (gt  "casedist" ) dnames;
  14.115 -  val con_rews  = List.concat (map (gts "con_rews" ) dnames);
  14.116 -  val copy_rews = List.concat (map (gts "copy_rews") dnames);
  14.117 +  val con_rews  = maps (gts "con_rews" ) dnames;
  14.118 +  val copy_rews = maps (gts "copy_rews") dnames;
  14.119  end;
  14.120  
  14.121  fun dc_take dn = %%:(dn^"_take");
  14.122 @@ -668,7 +668,7 @@
  14.123            val rhs = con_app2 con (app_rec_arg mk_take) args;
  14.124          in Library.foldr mk_all (map vname args, lhs === rhs) end;
  14.125        fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
  14.126 -      val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
  14.127 +      val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
  14.128        val simps = List.filter (has_fewer_prems 1) copy_rews;
  14.129        fun con_tac (con, args) =
  14.130          if nonlazy_rec args = []
  14.131 @@ -682,7 +682,7 @@
  14.132          simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
  14.133          asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
  14.134          TRY (safe_tac HOL_cs) ::
  14.135 -        List.concat (map eq_tacs eqs);
  14.136 +        maps eq_tacs eqs;
  14.137      in pg copy_take_defs goal tacs end;
  14.138  in
  14.139    val take_rews = map standard
  14.140 @@ -709,14 +709,14 @@
  14.141      (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
  14.142  
  14.143    fun ind_prems_tac prems = EVERY
  14.144 -    (List.concat (map (fn cons =>
  14.145 +    (maps (fn cons =>
  14.146        (resolve_tac prems 1 ::
  14.147 -        List.concat (map (fn (_,args) => 
  14.148 +        maps (fn (_,args) => 
  14.149            resolve_tac prems 1 ::
  14.150            map (K(atac 1)) (nonlazy args) @
  14.151            map (K(atac 1)) (List.filter is_rec args))
  14.152 -        cons)))
  14.153 -      conss));
  14.154 +        cons))
  14.155 +      conss);
  14.156    local 
  14.157      (* check whether every/exists constructor of the n-th part of the equation:
  14.158         it has a possibly indirectly recursive argument that isn't/is possibly 
  14.159 @@ -765,9 +765,9 @@
  14.160            fun cases_tacs (cons, cases) =
  14.161              res_inst_tac [("x","x")] cases 1 ::
  14.162              asm_simp_tac (take_ss addsimps prems) 1 ::
  14.163 -            List.concat (map con_tacs cons);
  14.164 +            maps con_tacs cons;
  14.165          in
  14.166 -          tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
  14.167 +          tacs1 @ maps cases_tacs (conss ~~ cases)
  14.168          end;
  14.169      in pg'' thy [] goal tacf end;
  14.170  
  14.171 @@ -836,19 +836,19 @@
  14.172                asm_simp_tac take_ss 1];
  14.173              fun con_tacs (con, args) =
  14.174                asm_simp_tac take_ss 1 ::
  14.175 -              List.concat (map arg_tacs (nonlazy_rec args));
  14.176 +              maps arg_tacs (nonlazy_rec args);
  14.177              fun foo_tacs n (cons, cases) =
  14.178                simp_tac take_ss 1 ::
  14.179                rtac allI 1 ::
  14.180                res_inst_tac [("x",x_name n)] cases 1 ::
  14.181                asm_simp_tac take_ss 1 ::
  14.182 -              List.concat (map con_tacs cons);
  14.183 +              maps con_tacs cons;
  14.184              val tacs =
  14.185                rtac allI 1 ::
  14.186                induct_tac "n" 1 ::
  14.187                simp_tac take_ss 1 ::
  14.188                TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
  14.189 -              List.concat (mapn foo_tacs 1 (conss ~~ cases));
  14.190 +              flat (mapn foo_tacs 1 (conss ~~ cases));
  14.191            in pg [] goal tacs end;
  14.192  
  14.193          fun one_finite (dn, l1b) =
  14.194 @@ -876,7 +876,7 @@
  14.195                    ind_prems_tac prems];
  14.196                in
  14.197                  TRY (safe_tac HOL_cs) ::
  14.198 -                List.concat (map finite_tacs (finites ~~ atomize finite_ind))
  14.199 +                maps finite_tacs (finites ~~ atomize finite_ind)
  14.200                end;
  14.201            in pg'' thy [] (ind_term concf) tacf end;
  14.202        in (finites, ind) end (* let *)
  14.203 @@ -941,7 +941,7 @@
  14.204          induct_tac "n" 1,
  14.205          simp_tac take_ss 1,
  14.206          safe_tac HOL_cs] @
  14.207 -        List.concat (mapn x_tacs 0 xs);
  14.208 +        flat (mapn x_tacs 0 xs);
  14.209      in pg [ax_bisim_def] goal tacs end;
  14.210  in
  14.211    val coind = 
  14.212 @@ -954,11 +954,11 @@
  14.213              mk_trp (foldr1 mk_conj (map mk_eqn xs)));
  14.214        val tacs =
  14.215          TRY (safe_tac HOL_cs) ::
  14.216 -        List.concat (map (fn take_lemma => [
  14.217 +        maps (fn take_lemma => [
  14.218            rtac take_lemma 1,
  14.219            cut_facts_tac [coind_lemma] 1,
  14.220            fast_tac HOL_cs 1])
  14.221 -        take_lemmas);
  14.222 +        take_lemmas;
  14.223      in pg [] goal tacs end;
  14.224  end; (* local *)
  14.225  
    15.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 18:15:25 2008 +0100
    15.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 22:27:57 2008 +0100
    15.3 @@ -267,7 +267,7 @@
    15.4      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
    15.5      val cname = case chead_of t of Const(c,_) => c | _ =>
    15.6                fixrec_err "function is not declared as constant in theory";
    15.7 -    val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
    15.8 +    val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
    15.9      val simp = Goal.prove_global thy [] [] eq
   15.10            (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   15.11    in simp end;
    16.1 --- a/src/Pure/Isar/args.ML	Wed Mar 19 18:15:25 2008 +0100
    16.2 +++ b/src/Pure/Isar/args.ML	Wed Mar 19 22:27:57 2008 +0100
    16.3 @@ -82,7 +82,7 @@
    16.4    val tyname: Context.generic * T list -> string * (Context.generic * T list)
    16.5    val const: Context.generic * T list -> string * (Context.generic * T list)
    16.6    val const_proper: Context.generic * T list -> string * (Context.generic * T list)
    16.7 -  val thm_sel: T list -> PureThy.interval list * T list
    16.8 +  val thm_sel: T list -> Facts.interval list * T list
    16.9    val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
   16.10    val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
   16.11      -> ((int -> tactic) -> tactic) * ('a * T list)
   16.12 @@ -344,9 +344,9 @@
   16.13  (* misc *)
   16.14  
   16.15  val thm_sel = parens (list1
   16.16 - (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
   16.17 -  nat --| $$$ "-" >> PureThy.From ||
   16.18 -  nat >> PureThy.Single));
   16.19 + (nat --| $$$ "-" -- nat >> Facts.FromTo ||
   16.20 +  nat --| $$$ "-" >> Facts.From ||
   16.21 +  nat >> Facts.Single));
   16.22  
   16.23  val bang_facts = Scan.peek (fn context =>
   16.24    $$$ "!" >> (fn _ => (warning "use of prems in proof method";
    17.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 19 18:15:25 2008 +0100
    17.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 19 22:27:57 2008 +0100
    17.3 @@ -19,7 +19,7 @@
    17.4    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    17.5    val attribute: theory -> src -> attribute
    17.6    val attribute_i: theory -> src -> attribute
    17.7 -  val eval_thms: Proof.context -> (thmref * src list) list -> thm list
    17.8 +  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    17.9    val map_specs: ('a -> 'att) ->
   17.10      (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
   17.11    val map_facts: ('a -> 'att) ->
   17.12 @@ -157,34 +157,36 @@
   17.13  
   17.14  local
   17.15  
   17.16 -val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
   17.17 -
   17.18  val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
   17.19  
   17.20 -fun gen_thm pick = Scan.depend (fn st =>
   17.21 -  Args.$$$ "[" |-- Args.attribs (intern (Context.theory_of st)) --| Args.$$$ "]"
   17.22 -    >> (fn srcs =>
   17.23 +fun gen_thm pick = Scan.depend (fn context =>
   17.24 +  let
   17.25 +    val thy = Context.theory_of context;
   17.26 +    val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
   17.27 +    fun get_fact s = get (Facts.Fact s);
   17.28 +    fun get_named s = get (Facts.Named (s, NONE));
   17.29 +  in
   17.30 +    Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
   17.31        let
   17.32 -        val atts = map (attribute_i (Context.theory_of st)) srcs;
   17.33 -        val (st', th') = Library.apply atts (st, Drule.dummy_thm);
   17.34 -      in (st', pick "" [th']) end) ||
   17.35 -  (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
   17.36 -    >> (fn (s, fact) => ("", Fact s, fact)) ||
   17.37 -  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
   17.38 -    >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
   17.39 -  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name)
   17.40 -    >> (fn (name, fact) => (name, Name name, fact)))
   17.41 -  -- Args.opt_attribs (intern (Context.theory_of st))
   17.42 -  >> (fn ((name, thmref, fact), srcs) =>
   17.43 -    let
   17.44 -      val ths = PureThy.select_thm thmref fact;
   17.45 -      val atts = map (attribute_i (Context.theory_of st)) srcs;
   17.46 -      val (st', ths') = foldl_map (Library.apply atts) (st, ths);
   17.47 -    in (st', pick name ths') end));
   17.48 +        val atts = map (attribute_i thy) srcs;
   17.49 +        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
   17.50 +      in (context', pick "" [th']) end)
   17.51 +    ||
   17.52 +    (Scan.ahead Args.alt_name -- Args.named_fact get_fact
   17.53 +      >> (fn (s, fact) => ("", Facts.Fact s, fact))
   17.54 +    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
   17.55 +      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
   17.56 +    -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
   17.57 +      let
   17.58 +        val ths = Facts.select thmref fact;
   17.59 +        val atts = map (attribute_i thy) srcs;
   17.60 +        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
   17.61 +      in (context', pick name ths') end)
   17.62 +  end);
   17.63  
   17.64  in
   17.65  
   17.66 -val thm = gen_thm PureThy.single_thm;
   17.67 +val thm = gen_thm Facts.the_single;
   17.68  val multi_thm = gen_thm (K I);
   17.69  val thms = Scan.repeat multi_thm >> flat;
   17.70  
    18.1 --- a/src/Pure/Isar/calculation.ML	Wed Mar 19 18:15:25 2008 +0100
    18.2 +++ b/src/Pure/Isar/calculation.ML	Wed Mar 19 22:27:57 2008 +0100
    18.3 @@ -14,9 +14,9 @@
    18.4    val sym_add: attribute
    18.5    val sym_del: attribute
    18.6    val symmetric: attribute
    18.7 -  val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    18.8 +  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    18.9    val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   18.10 -  val finally_: (thmref * Attrib.src list) list option -> bool ->
   18.11 +  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
   18.12      Proof.state -> Proof.state Seq.seq
   18.13    val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   18.14    val moreover: bool -> Proof.state -> Proof.state
    19.1 --- a/src/Pure/Isar/element.ML	Wed Mar 19 18:15:25 2008 +0100
    19.2 +++ b/src/Pure/Isar/element.ML	Wed Mar 19 22:27:57 2008 +0100
    19.3 @@ -11,16 +11,16 @@
    19.4    datatype ('typ, 'term) stmt =
    19.5      Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
    19.6      Obtains of (string * ((string * 'typ option) list * 'term list)) list
    19.7 -  type statement  (*= (string, string) stmt*)
    19.8 -  type statement_i  (*= (typ, term) stmt*)
    19.9 +  type statement = (string, string) stmt
   19.10 +  type statement_i = (typ, term) stmt
   19.11    datatype ('typ, 'term, 'fact) ctxt =
   19.12      Fixes of (string * 'typ option * mixfix) list |
   19.13      Constrains of (string * 'typ) list |
   19.14      Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
   19.15      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
   19.16      Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
   19.17 -  type context (*= (string, string, thmref) ctxt*)
   19.18 -  type context_i (*= (typ, term, thm list) ctxt*)
   19.19 +  type context = (string, string, Facts.ref) ctxt
   19.20 +  type context_i = (typ, term, thm list) ctxt
   19.21    val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
   19.22     ((string * Attrib.src list) * ('fact * Attrib.src list) list) list ->
   19.23     ((string * Attrib.src list) * ('c * Attrib.src list) list) list
   19.24 @@ -99,7 +99,7 @@
   19.25    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
   19.26    Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
   19.27  
   19.28 -type context = (string, string, thmref) ctxt;
   19.29 +type context = (string, string, Facts.ref) ctxt;
   19.30  type context_i = (typ, term, thm list) ctxt;
   19.31  
   19.32  fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
    20.1 --- a/src/Pure/Isar/find_theorems.ML	Wed Mar 19 18:15:25 2008 +0100
    20.2 +++ b/src/Pure/Isar/find_theorems.ML	Wed Mar 19 22:27:57 2008 +0100
    20.3 @@ -49,7 +49,7 @@
    20.4  (** search criterion filters **)
    20.5  
    20.6  (*generated filters are to be of the form
    20.7 -  input: (thmref * thm)
    20.8 +  input: (Facts.ref * thm)
    20.9    output: (p:int, s:int) option, where
   20.10      NONE indicates no match
   20.11      p is the primary sorting criterion
   20.12 @@ -107,7 +107,7 @@
   20.13    in match (space_explode "*" pat) str end;
   20.14  
   20.15  fun filter_name str_pat (thmref, _) =
   20.16 -  if match_string str_pat (PureThy.name_of_thmref thmref)
   20.17 +  if match_string str_pat (Facts.name_of_ref thmref)
   20.18    then SOME (0, 0) else NONE;
   20.19  
   20.20  
   20.21 @@ -243,42 +243,36 @@
   20.22      EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
   20.23    | ord => ord) <> GREATER;
   20.24  
   20.25 -in
   20.26 +fun nicer (Facts.Named (x, _)) (Facts.Named (y, _)) = nicer_name x y
   20.27 +  | nicer (Facts.Fact _) (Facts.Named _) = true
   20.28 +  | nicer (Facts.Named _) (Facts.Fact _) = false;
   20.29  
   20.30 -fun nicer (Fact _) _ = true
   20.31 -  | nicer (PureThy.Name x) (PureThy.Name y) = nicer_name x y
   20.32 -  | nicer (PureThy.Name _) (Fact _) = false
   20.33 -  | nicer (PureThy.Name _) _ = true
   20.34 -  | nicer (NameSelection (x, _)) (NameSelection (y, _)) = nicer_name x y
   20.35 -  | nicer (NameSelection _) _ = false;
   20.36 +fun rem_cdups xs =
   20.37 +  let
   20.38 +    fun rem_c rev_seen [] = rev rev_seen
   20.39 +      | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
   20.40 +      | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
   20.41 +        if Thm.eq_thm_prop (t, t')
   20.42 +        then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
   20.43 +        else rem_c (x :: rev_seen) (y :: xs)
   20.44 +  in rem_c [] xs end;
   20.45  
   20.46 -end;
   20.47 +in
   20.48  
   20.49  fun rem_thm_dups xs =
   20.50 -  let
   20.51 -    fun rem_cdups xs =
   20.52 -      let
   20.53 -        fun rem_c rev_seen [] = rev rev_seen
   20.54 -          | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
   20.55 -          | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
   20.56 -            if Thm.eq_thm_prop (t, t')
   20.57 -            then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
   20.58 -            else rem_c (x :: rev_seen) (y :: xs)
   20.59 -      in rem_c [] xs end;
   20.60 +  xs ~~ (1 upto length xs)
   20.61 +  |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   20.62 +  |> rem_cdups
   20.63 +  |> sort (int_ord o pairself #2)
   20.64 +  |> map #1;
   20.65  
   20.66 -  in
   20.67 -    xs ~~ (1 upto length xs)
   20.68 -    |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   20.69 -    |> rem_cdups
   20.70 -    |> sort (int_ord o pairself #2)
   20.71 -    |> map #1
   20.72 -  end;
   20.73 +end;
   20.74  
   20.75  
   20.76  (* print_theorems *)
   20.77  
   20.78  fun all_facts_of ctxt =
   20.79 -  maps PureThy.selections
   20.80 +  maps Facts.selections
   20.81     (Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @
   20.82      Facts.dest (ProofContext.facts_of ctxt));
   20.83  
   20.84 @@ -300,7 +294,7 @@
   20.85      val thms = Library.drop (len - lim, matches);
   20.86  
   20.87      fun prt_fact (thmref, thm) =
   20.88 -      ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
   20.89 +      ProofContext.pretty_fact ctxt (Facts.string_of_ref thmref, [thm]);
   20.90    in
   20.91      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
   20.92       (if null thms then [Pretty.str "nothing found"]
    21.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 19 18:15:25 2008 +0100
    21.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 19 22:27:57 2008 +0100
    21.3 @@ -17,7 +17,7 @@
    21.4    val oracle: bstring -> string -> string -> theory -> theory
    21.5    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    21.6    val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    21.7 -  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    21.8 +  val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
    21.9    val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
   21.10    val declaration: string -> local_theory -> local_theory
   21.11    val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
   21.12 @@ -91,18 +91,18 @@
   21.13    val print_antiquotations: Toplevel.transition -> Toplevel.transition
   21.14    val class_deps: Toplevel.transition -> Toplevel.transition
   21.15    val thy_deps: Toplevel.transition -> Toplevel.transition
   21.16 -  val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   21.17 +  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   21.18    val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
   21.19      -> Toplevel.transition -> Toplevel.transition
   21.20    val unused_thms: (string list * string list option) option ->
   21.21      Toplevel.transition -> Toplevel.transition
   21.22    val print_binds: Toplevel.transition -> Toplevel.transition
   21.23    val print_cases: Toplevel.transition -> Toplevel.transition
   21.24 -  val print_stmts: string list * (thmref * Attrib.src list) list
   21.25 +  val print_stmts: string list * (Facts.ref * Attrib.src list) list
   21.26      -> Toplevel.transition -> Toplevel.transition
   21.27 -  val print_thms: string list * (thmref * Attrib.src list) list
   21.28 +  val print_thms: string list * (Facts.ref * Attrib.src list) list
   21.29      -> Toplevel.transition -> Toplevel.transition
   21.30 -  val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
   21.31 +  val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
   21.32      -> Toplevel.transition -> Toplevel.transition
   21.33    val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   21.34    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    22.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 19 18:15:25 2008 +0100
    22.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 19 22:27:57 2008 +0100
    22.3 @@ -60,18 +60,18 @@
    22.4      ((string * mixfix) * (term * term list))) list -> state -> state
    22.5    val chain: state -> state
    22.6    val chain_facts: thm list -> state -> state
    22.7 -  val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
    22.8 +  val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
    22.9    val note_thmss: ((string * Attrib.src list) *
   22.10 -    (thmref * Attrib.src list) list) list -> state -> state
   22.11 +    (Facts.ref * Attrib.src list) list) list -> state -> state
   22.12    val note_thmss_i: ((string * attribute list) *
   22.13      (thm list * attribute list) list) list -> state -> state
   22.14 -  val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
   22.15 +  val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   22.16    val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   22.17 -  val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
   22.18 +  val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   22.19    val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
   22.20 -  val using: ((thmref * Attrib.src list) list) list -> state -> state
   22.21 +  val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
   22.22    val using_i: ((thm list * attribute list) list) list -> state -> state
   22.23 -  val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
   22.24 +  val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
   22.25    val unfolding_i: ((thm list * attribute list) list) list -> state -> state
   22.26    val invoke_case: string * string option list * Attrib.src list -> state -> state
   22.27    val invoke_case_i: string * string option list * attribute list -> state -> state
    23.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 19 18:15:25 2008 +0100
    23.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 19 22:27:57 2008 +0100
    23.3 @@ -91,8 +91,8 @@
    23.4      -> Proof.context * (term list list * (Proof.context -> Proof.context))
    23.5    val fact_tac: thm list -> int -> tactic
    23.6    val some_fact_tac: Proof.context -> int -> tactic
    23.7 -  val get_thm: Proof.context -> thmref -> thm
    23.8 -  val get_thms: Proof.context -> thmref -> thm list
    23.9 +  val get_thm: Proof.context -> Facts.ref -> thm
   23.10 +  val get_thms: Proof.context -> Facts.ref -> thm list
   23.11    val valid_thms: Proof.context -> string * thm list -> bool
   23.12    val add_path: string -> Proof.context -> Proof.context
   23.13    val no_base_names: Proof.context -> Proof.context
   23.14 @@ -102,7 +102,7 @@
   23.15    val reset_naming: Proof.context -> Proof.context
   23.16    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   23.17    val note_thmss: string ->
   23.18 -    ((bstring * attribute list) * (thmref * attribute list) list) list ->
   23.19 +    ((bstring * attribute list) * (Facts.ref * attribute list) list) list ->
   23.20        Proof.context -> (bstring * thm list) list * Proof.context
   23.21    val note_thmss_i: string ->
   23.22      ((bstring * attribute list) * (thm list * attribute list) list) list ->
   23.23 @@ -790,7 +790,7 @@
   23.24  
   23.25  (* get_thm(s) *)
   23.26  
   23.27 -fun retrieve_thms _ pick ctxt (Fact s) =
   23.28 +fun retrieve_thms _ pick ctxt (Facts.Fact s) =
   23.29        let
   23.30          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
   23.31            |> singleton (Variable.polymorphic ctxt);
   23.32 @@ -802,17 +802,17 @@
   23.33          val thy = theory_of ctxt;
   23.34          val local_facts = facts_of ctxt;
   23.35          val space = Facts.space_of local_facts;
   23.36 -        val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
   23.37 -        val name = PureThy.name_of_thmref thmref;
   23.38 +        val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
   23.39 +        val name = Facts.name_of_ref thmref;
   23.40          val thms =
   23.41            if name = "" then [Thm.transfer thy Drule.dummy_thm]
   23.42            else
   23.43              (case Facts.lookup local_facts name of
   23.44 -              SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
   23.45 +              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
   23.46              | NONE => from_thy thy xthmref);
   23.47        in pick name thms end;
   23.48  
   23.49 -val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
   23.50 +val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
   23.51  val get_thms = retrieve_thms PureThy.get_thms (K I);
   23.52  val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
   23.53  
   23.54 @@ -820,7 +820,7 @@
   23.55  (* valid_thms *)
   23.56  
   23.57  fun valid_thms ctxt (name, ths) =
   23.58 -  (case try (fn () => get_thms_silent ctxt (Name name)) () of
   23.59 +  (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
   23.60      NONE => false
   23.61    | SOME ths' => Thm.eq_thms (ths, ths'));
   23.62  
    24.1 --- a/src/Pure/Isar/proof_display.ML	Wed Mar 19 18:15:25 2008 +0100
    24.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Mar 19 22:27:57 2008 +0100
    24.3 @@ -111,8 +111,9 @@
    24.4              if a <> "" then ((a, ths), j)
    24.5              else if m = n then ((name, ths), j)
    24.6              else if m = 1 then
    24.7 -              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
    24.8 -            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
    24.9 +              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
   24.10 +            else
   24.11 +              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
   24.12            end;
   24.13        in fst (fold_map name_res res 1) end;
   24.14  
    25.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Mar 19 18:15:25 2008 +0100
    25.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Mar 19 22:27:57 2008 +0100
    25.3 @@ -17,10 +17,10 @@
    25.4    val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    25.5    val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
    25.6    val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
    25.7 -  val xthm: token list -> (thmref * Attrib.src list) * token list
    25.8 -  val xthms1: token list -> (thmref * Attrib.src list) list * token list
    25.9 +  val xthm: token list -> (Facts.ref * Attrib.src list) * token list
   25.10 +  val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   25.11    val name_facts: token list ->
   25.12 -    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
   25.13 +    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
   25.14    val locale_mixfix: token list -> mixfix * token list
   25.15    val locale_fixes: token list -> (string * string option * mixfix) list * token list
   25.16    val locale_insts: token list ->
   25.17 @@ -65,13 +65,13 @@
   25.18  val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
   25.19  
   25.20  val thm_sel = P.$$$ "(" |-- P.list1
   25.21 - (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
   25.22 -  P.nat --| P.minus >> PureThy.From ||
   25.23 -  P.nat >> PureThy.Single) --| P.$$$ ")";
   25.24 + (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
   25.25 +  P.nat --| P.minus >> Facts.From ||
   25.26 +  P.nat >> Facts.Single) --| P.$$$ ")";
   25.27  
   25.28  val xthm =
   25.29 -  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
   25.30 -  (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
   25.31 +  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
   25.32 +  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
   25.33  
   25.34  val xthms1 = Scan.repeat1 xthm;
   25.35  
    26.1 --- a/src/Pure/Isar/specification.ML	Wed Mar 19 18:15:25 2008 +0100
    26.2 +++ b/src/Pure/Isar/specification.ML	Wed Mar 19 22:27:57 2008 +0100
    26.3 @@ -43,10 +43,11 @@
    26.4      local_theory -> local_theory
    26.5    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    26.6    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    26.7 -  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    26.8 -    -> local_theory -> (bstring * thm list) list * local_theory
    26.9 -  val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
   26.10 -    -> local_theory -> (bstring * thm list) list * local_theory
   26.11 +  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   26.12 +    local_theory -> (bstring * thm list) list * local_theory
   26.13 +  val theorems_cmd: string ->
   26.14 +    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
   26.15 +    local_theory -> (bstring * thm list) list * local_theory
   26.16    val theorem: string -> Method.text option ->
   26.17      (thm list list -> local_theory -> local_theory) ->
   26.18      string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    27.1 --- a/src/Pure/ML/ml_context.ML	Wed Mar 19 18:15:25 2008 +0100
    27.2 +++ b/src/Pure/ML/ml_context.ML	Wed Mar 19 22:27:57 2008 +0100
    27.3 @@ -264,21 +264,21 @@
    27.4  
    27.5  (** fact references **)
    27.6  
    27.7 -fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
    27.8 -fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
    27.9 +fun thm name = ProofContext.get_thm (the_local_context ()) (Facts.Named (name, NONE));
   27.10 +fun thms name = ProofContext.get_thms (the_local_context ()) (Facts.Named (name, NONE));
   27.11  
   27.12  
   27.13  local
   27.14  
   27.15 -fun print_interval (FromTo arg) =
   27.16 -      "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
   27.17 -  | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i
   27.18 -  | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i;
   27.19 +fun print_interval (Facts.FromTo arg) =
   27.20 +      "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
   27.21 +  | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
   27.22 +  | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
   27.23  
   27.24  fun thm_sel name =
   27.25 -  Args.thm_sel >> (fn is => "PureThy.NameSelection " ^
   27.26 -    ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is))
   27.27 -  || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name);
   27.28 +  Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
   27.29 +    ML_Syntax.print_pair ML_Syntax.print_string
   27.30 +      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
   27.31  
   27.32  fun thm_antiq kind = value_antiq kind
   27.33    (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
    28.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 19 18:15:25 2008 +0100
    28.2 +++ b/src/Pure/Proof/extraction.ML	Wed Mar 19 22:27:57 2008 +0100
    28.3 @@ -766,7 +766,7 @@
    28.4      (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
    28.5       (fn xs => Toplevel.theory (fn thy => add_realizers
    28.6         (map (fn (((a, vs), s1), s2) =>
    28.7 -         (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
    28.8 +         (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
    28.9  
   28.10  val _ =
   28.11    OuterSyntax.command "realizability"
   28.12 @@ -780,8 +780,8 @@
   28.13  
   28.14  val _ =
   28.15    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   28.16 -    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
   28.17 -      (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
   28.18 +    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   28.19 +      extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
   28.20  
   28.21  val etype_of = etype_of o add_syntax;
   28.22  
    29.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 18:15:25 2008 +0100
    29.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 22:27:57 2008 +0100
    29.3 @@ -712,7 +712,7 @@
    29.4                     What we want is mapping onto simple PGIP name/context model. *)
    29.5                  val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
    29.6                  val thy = Context.theory_of_proof ctx
    29.7 -                val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
    29.8 +                val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
    29.9                  val deps = filter_out (equal "")
   29.10                                        (Symtab.keys (fold Proofterm.thms_of_proof
   29.11                                                           (map Thm.proof_of ths) Symtab.empty))
   29.12 @@ -764,7 +764,7 @@
   29.13                                          [] (* asms *)
   29.14                                          th))
   29.15  
   29.16 -        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
   29.17 +        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
   29.18  
   29.19          val string_of_thy = Output.output o
   29.20                                  Pretty.string_of o (ProofDisplay.pretty_full_theory false)
    30.1 --- a/src/Pure/facts.ML	Wed Mar 19 18:15:25 2008 +0100
    30.2 +++ b/src/Pure/facts.ML	Wed Mar 19 22:27:57 2008 +0100
    30.3 @@ -7,6 +7,16 @@
    30.4  
    30.5  signature FACTS =
    30.6  sig
    30.7 +  val the_single: string -> thm list -> thm
    30.8 +  datatype interval = FromTo of int * int | From of int | Single of int
    30.9 +  datatype ref =
   30.10 +    Named of string * interval list option |
   30.11 +    Fact of string
   30.12 +  val string_of_ref: ref -> string
   30.13 +  val name_of_ref: ref -> string
   30.14 +  val map_name_of_ref: (string -> string) -> ref -> ref
   30.15 +  val select: ref -> thm list -> thm list
   30.16 +  val selections: string * thm list -> (ref * thm) list
   30.17    type T
   30.18    val space_of: T -> NameSpace.T
   30.19    val lookup: T -> string -> thm list option
   30.20 @@ -24,7 +34,76 @@
   30.21  structure Facts: FACTS =
   30.22  struct
   30.23  
   30.24 -(* datatype *)
   30.25 +(** fact references **)
   30.26 +
   30.27 +fun the_single _ [th] : thm = th
   30.28 +  | the_single name _ = error ("Single theorem expected " ^ quote name);
   30.29 +
   30.30 +
   30.31 +(* datatype interval *)
   30.32 +
   30.33 +datatype interval =
   30.34 +  FromTo of int * int |
   30.35 +  From of int |
   30.36 +  Single of int;
   30.37 +
   30.38 +fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
   30.39 +  | string_of_interval (From i) = string_of_int i ^ "-"
   30.40 +  | string_of_interval (Single i) = string_of_int i;
   30.41 +
   30.42 +fun interval n iv =
   30.43 +  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
   30.44 +    (case iv of
   30.45 +      FromTo (i, j) => if i <= j then i upto j else err ()
   30.46 +    | From i => if i <= n then i upto n else err ()
   30.47 +    | Single i => [i])
   30.48 +  end;
   30.49 +
   30.50 +
   30.51 +(* datatype ref *)
   30.52 +
   30.53 +datatype ref =
   30.54 +  Named of string * interval list option |
   30.55 +  Fact of string;
   30.56 +
   30.57 +fun name_of_ref (Named (name, _)) = name
   30.58 +  | name_of_ref (Fact _) = error "Illegal literal fact";
   30.59 +
   30.60 +fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
   30.61 +  | map_name_of_ref _ r = r;
   30.62 +
   30.63 +fun string_of_ref (Named (name, NONE)) = name
   30.64 +  | string_of_ref (Named (name, SOME is)) =
   30.65 +      name ^ enclose "(" ")" (commas (map string_of_interval is))
   30.66 +  | string_of_ref (Fact _) = error "Illegal literal fact";
   30.67 +
   30.68 +
   30.69 +(* select *)
   30.70 +
   30.71 +fun select (Fact _) ths = ths
   30.72 +  | select (Named (_, NONE)) ths = ths
   30.73 +  | select (Named (name, SOME ivs)) ths =
   30.74 +      let
   30.75 +        val n = length ths;
   30.76 +        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
   30.77 +        fun sel i =
   30.78 +          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
   30.79 +          else nth ths (i - 1);
   30.80 +        val is = maps (interval n) ivs handle Fail msg => err msg;
   30.81 +      in map sel is end;
   30.82 +
   30.83 +
   30.84 +(* selections *)
   30.85 +
   30.86 +fun selections (name, [th]) = [(Named (name, NONE), th)]
   30.87 +  | selections (name, ths) =
   30.88 +      map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
   30.89 +
   30.90 +
   30.91 +
   30.92 +(** fact environment **)
   30.93 +
   30.94 +(* datatype T *)
   30.95  
   30.96  datatype T = Facts of
   30.97   {facts: thm list NameSpace.table,
    31.1 --- a/src/Pure/pure_thy.ML	Wed Mar 19 18:15:25 2008 +0100
    31.2 +++ b/src/Pure/pure_thy.ML	Wed Mar 19 22:27:57 2008 +0100
    31.3 @@ -7,14 +7,8 @@
    31.4  
    31.5  signature BASIC_PURE_THY =
    31.6  sig
    31.7 -  datatype interval = FromTo of int * int | From of int | Single of int
    31.8 -  datatype thmref =
    31.9 -    Name of string |
   31.10 -    NameSelection of string * interval list |
   31.11 -    Fact of string
   31.12 -  val get_thm: theory -> thmref -> thm
   31.13 -  val get_thms: theory -> thmref -> thm list
   31.14 -  val get_thmss: theory -> thmref list -> thm list
   31.15 +  val get_thm: theory -> Facts.ref -> thm
   31.16 +  val get_thms: theory -> Facts.ref -> thm list
   31.17    structure ProtoPure:
   31.18      sig
   31.19        val thy: theory
   31.20 @@ -44,13 +38,7 @@
   31.21    val kind_internal: attribute
   31.22    val has_internal: Markup.property list -> bool
   31.23    val is_internal: thm -> bool
   31.24 -  val string_of_thmref: thmref -> string
   31.25 -  val single_thm: string -> thm list -> thm
   31.26 -  val name_of_thmref: thmref -> string
   31.27 -  val map_name_of_thmref: (string -> string) -> thmref -> thmref
   31.28 -  val select_thm: thmref -> thm list -> thm list
   31.29 -  val selections: string * thm list -> (thmref * thm) list
   31.30 -  val get_thms_silent: theory -> thmref -> thm list
   31.31 +  val get_thms_silent: theory -> Facts.ref -> thm list
   31.32    val theorems_of: theory -> thm list NameSpace.table
   31.33    val all_facts_of: theory -> Facts.T
   31.34    val thms_of: theory -> (string * thm) list
   31.35 @@ -73,7 +61,7 @@
   31.36    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   31.37    val note: string -> string * thm -> theory -> thm * theory
   31.38    val note_thmss: string -> ((bstring * attribute list) *
   31.39 -    (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   31.40 +    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   31.41    val note_thmss_i: string -> ((bstring * attribute list) *
   31.42      (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   31.43    val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
   31.44 @@ -182,75 +170,6 @@
   31.45  fun the_thms _ (SOME thms) = thms
   31.46    | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
   31.47  
   31.48 -fun single_thm _ [thm] = thm
   31.49 -  | single_thm name _ = error ("Single theorem expected " ^ quote name);
   31.50 -
   31.51 -
   31.52 -(* datatype interval *)
   31.53 -
   31.54 -datatype interval =
   31.55 -  FromTo of int * int |
   31.56 -  From of int |
   31.57 -  Single of int;
   31.58 -
   31.59 -fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
   31.60 -  | string_of_interval (From i) = string_of_int i ^ "-"
   31.61 -  | string_of_interval (Single i) = string_of_int i;
   31.62 -
   31.63 -fun interval n iv =
   31.64 -  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
   31.65 -    (case iv of
   31.66 -      FromTo (i, j) => if i <= j then i upto j else err ()
   31.67 -    | From i => if i <= n then i upto n else err ()
   31.68 -    | Single i => [i])
   31.69 -  end;
   31.70 -
   31.71 -
   31.72 -(* datatype thmref *)
   31.73 -
   31.74 -datatype thmref =
   31.75 -  Name of string |
   31.76 -  NameSelection of string * interval list |
   31.77 -  Fact of string;
   31.78 -
   31.79 -fun name_of_thmref (Name name) = name
   31.80 -  | name_of_thmref (NameSelection (name, _)) = name
   31.81 -  | name_of_thmref (Fact _) = error "Illegal literal fact";
   31.82 -
   31.83 -fun map_name_of_thmref f (Name name) = Name (f name)
   31.84 -  | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
   31.85 -  | map_name_of_thmref _ thmref = thmref;
   31.86 -
   31.87 -fun string_of_thmref (Name name) = name
   31.88 -  | string_of_thmref (NameSelection (name, is)) =
   31.89 -      name ^ enclose "(" ")" (commas (map string_of_interval is))
   31.90 -  | string_of_thmref (Fact _) = error "Illegal literal fact";
   31.91 -
   31.92 -
   31.93 -(* select_thm *)
   31.94 -
   31.95 -fun select_thm (Name _) thms = thms
   31.96 -  | select_thm (Fact _) thms = thms
   31.97 -  | select_thm (NameSelection (name, ivs)) thms =
   31.98 -      let
   31.99 -        val n = length thms;
  31.100 -        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
  31.101 -        fun select i =
  31.102 -          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
  31.103 -          else nth thms (i - 1);
  31.104 -        val is = maps (interval n) ivs handle Fail msg => err msg;
  31.105 -      in map select is end;
  31.106 -
  31.107 -
  31.108 -(* selections *)
  31.109 -
  31.110 -fun selections (name, [thm]) = [(Name name, thm)]
  31.111 -  | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
  31.112 -      (NameSelection (name, [Single i]), thm));
  31.113 -
  31.114 -
  31.115 -(* lookup/get thms *)
  31.116 -
  31.117  local
  31.118  
  31.119  fun lookup_thms thy xname =
  31.120 @@ -270,7 +189,7 @@
  31.121  
  31.122  fun get_fact silent theory thmref =
  31.123    let
  31.124 -    val name = name_of_thmref thmref;
  31.125 +    val name = Facts.name_of_ref thmref;
  31.126      val new_res = lookup_fact theory name;
  31.127      val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
  31.128      val is_same =
  31.129 @@ -283,14 +202,13 @@
  31.130        else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
  31.131          show_result new_res ^ " vs " ^ show_result old_res ^
  31.132          Position.str_of (Position.thread_data ()));
  31.133 -  in Option.map #2 old_res |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end;
  31.134 +  in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
  31.135  
  31.136  in
  31.137  
  31.138  val get_thms_silent = get_fact true;
  31.139  val get_thms = get_fact false;
  31.140 -fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
  31.141 -fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
  31.142 +fun get_thm thy thmref = Facts.the_single (Facts.name_of_ref thmref) (get_thms thy thmref);
  31.143  
  31.144  end;
  31.145  
    32.1 --- a/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 18:15:25 2008 +0100
    32.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 22:27:57 2008 +0100
    32.3 @@ -192,10 +192,10 @@
    32.4  fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
    32.5  
    32.6  local
    32.7 -    fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname)
    32.8 +    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
    32.9      val eq_th = get_thm "HOL.eq_reflection"
   32.10  in
   32.11 -  fun eq_to_meta th = (eq_th OF [th] handle _ => th)
   32.12 +  fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
   32.13  end
   32.14  
   32.15  
    33.1 --- a/src/Tools/code/code_package.ML	Wed Mar 19 18:15:25 2008 +0100
    33.2 +++ b/src/Tools/code/code_package.ML	Wed Mar 19 22:27:57 2008 +0100
    33.3 @@ -187,7 +187,7 @@
    33.4          val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
    33.5          val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
    33.6          val tfree_vars = map Logic.mk_type tfrees';
    33.7 -        val c = PureThy.string_of_thmref thmref
    33.8 +        val c = Facts.string_of_ref thmref
    33.9            |> NameSpace.explode
   33.10            |> (fn [x] => [x] | (x::xs) => xs)
   33.11            |> space_implode "_"
   33.12 @@ -195,7 +195,7 @@
   33.13        in if c = "" then NONE else SOME (thmref, propdef) end;
   33.14    in
   33.15      Facts.dest (PureThy.all_facts_of thy)
   33.16 -    |> maps PureThy.selections
   33.17 +    |> maps Facts.selections
   33.18      |> map_filter select
   33.19      |> map_filter mk_codeprop
   33.20    end;
   33.21 @@ -206,7 +206,7 @@
   33.22      fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
   33.23      fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
   33.24        let
   33.25 -        val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
   33.26 +        val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
   33.27            ^ " as code property " ^ quote raw_c);
   33.28          val ([raw_c'], names') = Name.variants [raw_c] names;
   33.29          val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
    34.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Mar 19 18:15:25 2008 +0100
    34.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Mar 19 22:27:57 2008 +0100
    34.3 @@ -33,8 +33,8 @@
    34.4    val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
    34.5      thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    34.6    val add_datatype: string * string list -> (string * string list * mixfix) list list ->
    34.7 -    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
    34.8 -    (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
    34.9 +    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
   34.10 +    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
   34.11  end;
   34.12  
   34.13  functor Add_datatype_def_Fun
    35.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 18:15:25 2008 +0100
    35.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Mar 19 22:27:57 2008 +0100
    35.3 @@ -13,8 +13,8 @@
    35.4    val induct_tac: string -> int -> tactic
    35.5    val exhaust_tac: string -> int -> tactic
    35.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    35.7 -  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
    35.8 -    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
    35.9 +  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
   35.10 +    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
   35.11    val setup: theory -> theory
   35.12  end;
   35.13  
   35.14 @@ -167,8 +167,8 @@
   35.15  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   35.16    let
   35.17      val ctxt = ProofContext.init thy;
   35.18 -    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
   35.19 -    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
   35.20 +    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
   35.21 +    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
   35.22      val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
   35.23      val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   35.24    in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
    36.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Mar 19 18:15:25 2008 +0100
    36.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Mar 19 22:27:57 2008 +0100
    36.3 @@ -33,8 +33,8 @@
    36.4      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
    36.5    val add_inductive: string list * string ->
    36.6      ((bstring * string) * Attrib.src list) list ->
    36.7 -    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
    36.8 -    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
    36.9 +    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
   36.10 +    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
   36.11      theory -> theory * inductive_result
   36.12  end;
   36.13