# HG changeset patch
# User wenzelm
# Date 1394814731 -3600
# Node ID d94d6a9178b52f6cd3f380aec069438d523933a0
# Parent  64eeda68e693fde78ab28318ec791c51c16d5eb5# Parent  9589605bcf41811ec0c8aa085fccc25591223ce7
merged

diff -r 64eeda68e693 -r d94d6a9178b5 NEWS
--- a/NEWS	Fri Mar 14 12:09:51 2014 +0100
+++ b/NEWS	Fri Mar 14 17:32:11 2014 +0100
@@ -460,6 +460,12 @@
 * ML antiquotation @{here} refers to its source position, which is
 occasionally useful for experimentation and diagnostic purposes.
 
+* ML antiquotation @{path} produces a Path.T value, similarly to
+Path.explode, but with compile-time check against the file-system and
+some PIDE markup.  Note that unlike theory source, ML does not have a
+well-defined master directory, so an absolute symbolic path
+specification is usually required, e.g. "~~/src/HOL".
+
 
 *** System ***
 
diff -r 64eeda68e693 -r d94d6a9178b5 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Mar 14 12:09:51 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Mar 14 17:32:11 2014 +0100
@@ -367,6 +367,7 @@
     "hide_fact"
     "hide_type"
     "inductive"
+    "inductive_cases"
     "instantiation"
     "judgment"
     "lemmas"
@@ -404,7 +405,7 @@
     "typedecl"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("corollary"
diff -r 64eeda68e693 -r d94d6a9178b5 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Mar 14 12:09:51 2014 +0100
+++ b/etc/isar-keywords.el	Fri Mar 14 17:32:11 2014 +0100
@@ -532,7 +532,9 @@
     "import_tptp"
     "import_type_map"
     "inductive"
+    "inductive_cases"
     "inductive_set"
+    "inductive_simps"
     "instantiation"
     "judgment"
     "lemmas"
@@ -592,8 +594,7 @@
     "typedecl"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"
-    "inductive_simps"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
diff -r 64eeda68e693 -r d94d6a9178b5 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -166,12 +166,12 @@
   | parse_named _ _ = [];
 
 val jedit_actions =
-  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
+  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   | _ => []);
 
 val jedit_dockables =
-  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
+  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   | _ => []);
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -448,8 +448,8 @@
   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
 
 ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
-    error "thm int2.assoc was generated")
-  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
+    raise Fail "thm int2.assoc was generated")
+  handle ERROR _ => ([]:thm list); *}
 
 thm int.lone int.right.rone
   (* the latter comes through the sublocale relation *)
@@ -782,8 +782,8 @@
 context container begin
 ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
   val _ = Proof_Context.get_thms context "private.true" in generic end);
-  error "thm private.true was persisted")
-  handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
+  raise Fail "thm private.true was persisted")
+  handle ERROR _ => ([]:thm list); *}
 thm true_copy
 end
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -456,7 +456,7 @@
 text {*Usually, if this rule causes a failed congruence proof error,
   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   Adding @{thm [source] Pi_def} to the simpset is often useful.
-  For this reason, @{thm [source] comm_monoid.finprod_cong}
+  For this reason, @{thm [source] finprod_cong}
   is not added to the simpset by default.
 *}
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Inductive.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -7,8 +7,8 @@
 theory Inductive
 imports Complete_Lattices Ctr_Sugar
 keywords
-  "inductive" "coinductive" :: thy_decl and
-  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+  "monos" and
   "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -640,6 +640,11 @@
   shows "Max M \<le> Max N"
   using assms by (fact Max.antimono)
 
+end
+
+context linorder  (* FIXME *)
+begin
+
 lemma mono_Min_commute:
   assumes "mono f"
   assumes "finite A" and "A \<noteq> {}"
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Library/refute.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -1073,7 +1073,7 @@
               handle Option.Option =>
                      error ("Unknown SAT solver: " ^ quote satsolver ^
                             ". Available solvers: " ^
-                            commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
+                            commas (map (quote o fst) (SatSolver.get_solvers ())) ^ ".")
           in
             Output.urgent_message "Invoking SAT solver...";
             (case solver fm of
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -37,7 +37,7 @@
 
 ML {*
 fun mutation_testing_of (name, thy) =
-  (MutabelleExtra.random_seed := 1.0;
+  (MutabelleExtra.init_random 1.0;
   MutabelleExtra.thms_of false thy
   |> MutabelleExtra.take_random 200
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
@@ -50,7 +50,7 @@
 (*
 ML {*
 
-      MutabelleExtra.random_seed := 1.0;
+      MutabelleExtra.init_random 1.0;
       MutabelleExtra.thms_of true @{theory Complex_Main}
       |> MutabelleExtra.take_random 1000000
       |> (fn thms => List.drop (thms, 1000))
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -40,15 +40,12 @@
 val mutate_theorems_and_write_report :
   theory -> int * int -> mtd list -> thm list -> string -> unit
 
-val random_seed : real Unsynchronized.ref
+val init_random : real -> unit
 end;
 
 structure MutabelleExtra : MUTABELLE_EXTRA =
 struct
 
-(* Own seed; can't rely on the Isabelle one to stay the same *)
-val random_seed = Unsynchronized.ref 1.0;
-
 (* Another Random engine *)
 
 exception RANDOM;
@@ -56,13 +53,20 @@
 fun rmod x y = x - y * Real.realFloor (x / y);
 
 local
+  (* Own seed; can't rely on the Isabelle one to stay the same *)
+  val random_seed = Synchronized.var "random_seed" 1.0;
+
   val a = 16807.0;
   val m = 2147483647.0;
 in
 
-fun random () = CRITICAL (fn () =>
-  let val r = rmod (a * ! random_seed) m
-  in (random_seed := r; r) end);
+fun init_random r = Synchronized.change random_seed (K r);
+
+fun random () =
+  Synchronized.change_result random_seed
+    (fn s =>
+      let val r = rmod (a * s) m
+      in (r, r) end);
 
 end;
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -573,7 +573,7 @@
       let
         (* use the first ML solver (to avoid startup overhead) *)
         val (ml_solvers, nonml_solvers) =
-          !SatSolver.solvers
+          SatSolver.get_solvers ()
           |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
         val res =
           if null nonml_solvers then
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -200,10 +200,10 @@
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
 
 val pnf_narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
 
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -459,7 +459,7 @@
       else
         is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
-    val named_locals = local_facts |> Facts.dest_static []
+    val named_locals = local_facts |> Facts.dest_static [global_facts]
     val assms = Assumption.all_assms_of ctxt
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
diff -r 64eeda68e693 -r d94d6a9178b5 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -42,7 +42,7 @@
   val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
 
   (* generic solver interface *)
-  val solvers       : (string * solver) list Unsynchronized.ref
+  val get_solvers   : unit -> (string * solver) list
   val add_solver    : string * solver -> unit
   val invoke_solver : string -> solver  (* exception Option *)
 end;
@@ -348,22 +348,24 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
-(* solvers: a (reference to a) table of all registered SAT solvers           *)
+(* solvers: a table of all registered SAT solvers                            *)
 (* ------------------------------------------------------------------------- *)
 
-  val solvers = Unsynchronized.ref ([] : (string * solver) list);
+  val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
+
+  fun get_solvers () = Synchronized.value solvers;
 
 (* ------------------------------------------------------------------------- *)
 (* add_solver: updates 'solvers' by adding a new solver                      *)
 (* ------------------------------------------------------------------------- *)
 
-    fun add_solver (name, new_solver) = CRITICAL (fn () =>
+  fun add_solver (name, new_solver) =
+    Synchronized.change solvers (fn the_solvers =>
       let
-        val the_solvers = !solvers;
         val _ = if AList.defined (op =) the_solvers name
           then warning ("SAT solver " ^ quote name ^ " was defined before")
           else ();
-      in solvers := AList.update (op =) (name, new_solver) the_solvers end);
+      in AList.update (op =) (name, new_solver) the_solvers end);
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)
@@ -372,7 +374,7 @@
 (* ------------------------------------------------------------------------- *)
 
   fun invoke_solver name =
-    (the o AList.lookup (op =) (!solvers)) name;
+    the (AList.lookup (op =) (get_solvers ()) name);
 
 end;  (* SatSolver *)
 
@@ -521,7 +523,7 @@
           handle SatSolver.NOT_CONFIGURED => loop solvers
       )
   in
-    loop (!SatSolver.solvers)
+    loop (SatSolver.get_solvers ())
   end
 in
   SatSolver.add_solver ("auto", auto_solver)
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/General/change_table.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -17,6 +17,7 @@
   val empty: 'a T
   val is_empty: 'a T -> bool
   val change_base: bool -> 'a T -> 'a T
+  val change_ignore: 'a T -> 'a T
   val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
@@ -43,35 +44,42 @@
 
 (* optional change *)
 
-datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set};
+datatype change =
+  No_Change | Change of {base: serial, depth: int, changes: Table.set option};
 
 fun make_change base depth changes =
   Change {base = base, depth = depth, changes = changes};
 
+fun ignore_change (Change {base, depth, changes = SOME _}) =
+      make_change base depth NONE
+  | ignore_change change = change;
+
+fun update_change key (Change {base, depth, changes = SOME ch}) =
+      make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
+  | update_change _ change = change;
+
 fun base_change true No_Change =
-      make_change (serial ()) 0 Table.empty
+      make_change (serial ()) 0 (SOME Table.empty)
   | base_change true (Change {base, depth, changes}) =
       make_change base (depth + 1) changes
   | base_change false (Change {base, depth, changes}) =
       if depth = 0 then No_Change else make_change base (depth - 1) changes
-  | base_change false No_Change = raise Fail "Unbalanced block structure of change table";
+  | base_change false No_Change = raise Fail "Unbalanced change structure";
 
-fun update_change _ No_Change = No_Change
-  | update_change key (Change {base, depth, changes}) =
-      make_change base depth (Table.insert (K true) (key, ()) changes);
-
-fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
+fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure";
 
 fun merge_change (No_Change, No_Change) = NONE
   | merge_change (Change change1, Change change2) =
       let
         val {base = base1, depth = depth1, changes = changes1} = change1;
         val {base = base2, depth = depth2, changes = changes2} = change2;
-      in
-        if base1 = base2 andalso depth1 = depth2 then
-          SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
-        else cannot_merge ()
-      end
+        val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge ();
+        val (swapped, ch2) =
+          (case (changes1, changes2) of
+            (_, SOME ch2) => (false, ch2)
+          | (SOME ch1, _) => (true, ch1)
+          | _ => cannot_merge ());
+      in SOME (swapped, ch2, make_change base1 depth1 NONE) end
   | merge_change _ = cannot_merge ();
 
 
@@ -90,6 +98,7 @@
 fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
 
 fun change_base begin = (map_change_table o apfst) (base_change begin);
+fun change_ignore arg = (map_change_table o apfst) ignore_change arg;
 
 
 (* join and merge *)
@@ -105,20 +114,21 @@
     else
       (case merge_change (change1, change2) of
         NONE => make_change_table (No_Change, Table.join f (table1, table2))
-      | SOME (changes2, change') =>
+      | SOME (swapped, ch2, change') =>
           let
-            fun update key table =
-              (case Table.lookup table2 key of
-                NONE => table
+            fun maybe_swap (x, y) = if swapped then (y, x) else (x, y);
+            val (tab1, tab2) = maybe_swap (table1, table2);
+            fun update key tab =
+              (case Table.lookup tab2 key of
+                NONE => tab
               | SOME y =>
-                  (case Table.lookup table key of
-                    NONE => Table.update (key, y) table
+                  (case Table.lookup tab key of
+                    NONE => Table.update (key, y) tab
                   | SOME x =>
-                      (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
-                        NONE => table
-                      | SOME z => Table.update (key, z) table)));
-            val table' = Table.fold (update o #1) changes2 table1;
-          in make_change_table (change', table') end)
+                      (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
+                        NONE => tab
+                      | SOME z => Table.update (key, z) tab)));
+          in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
   end;
 
 fun merge eq =
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/General/name_space.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -56,6 +56,7 @@
   val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table
   val change_base: bool -> 'a table -> 'a table
+  val change_ignore: 'a table -> 'a table
   val space_of_table: 'a table -> T
   val check_reports: Context.generic -> 'a table ->
     xstring * Position.T list -> (string * Position.report list) * 'a
@@ -123,6 +124,9 @@
 fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
   (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
 
+val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
+  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
+
 fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
   (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
 
@@ -474,6 +478,9 @@
 fun change_base begin (Table (space, tab)) =
   Table (change_base_space begin space, Change_Table.change_base begin tab);
 
+fun change_ignore (Table (space, tab)) =
+  Table (change_ignore_space space, Change_Table.change_ignore tab);
+
 fun space_of_table (Table (space, _)) = space;
 
 fun check_reports context (Table (space, tab)) (xname, ps) =
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/General/path.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -30,6 +30,7 @@
   val ext: string -> T -> T
   val split_ext: T -> T * string
   val expand: T -> T
+  val smart_implode: T -> string
   val position: T -> Position.T
 end;
 
@@ -194,21 +195,26 @@
 val expand = rep #> maps eval #> norm #> Path;
 
 
-(* source position -- with smart replacement of ISABELLE_HOME *)
+(* smart implode *)
 
-val isabelle_home = explode_path "~~";
-
-fun position path =
+fun smart_implode path =
   let
-    val s = implode_path path;
-    val prfx = implode_path (expand isabelle_home) ^ "/";
+    val full_name = implode_path (expand path);
+    fun fold_path a =
+      let val b = implode_path (expand (explode_path a)) in
+        if full_name = b then SOME a
+        else
+          (case try (unprefix (b ^ "/")) full_name of
+            SOME name => SOME (a ^ "/" ^ name)
+          | NONE => NONE)
+      end;
   in
-    Position.file
-      (case try (unprefix prfx) s of
-        NONE => s
-      | SOME s' => "~~/" ^ s')
+    (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
+      SOME name => name
+    | NONE => implode_path path)
   end;
 
+val position = Position.file o smart_implode;
 
 (*final declarations of this structure!*)
 val implode = implode_path;
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -213,7 +213,7 @@
 
 fun gen_thm pick = Scan.depend (fn context =>
   let
-    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
+    val get = Proof_Context.get_fact_generic context;
     val get_fact = get o Facts.Fact;
     fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   in
@@ -249,6 +249,8 @@
 
 (** partial evaluation -- observing rule/declaration/mixed attributes **)
 
+(*NB: result length may change due to rearrangement of symbolic expression*)
+
 local
 
 fun apply_att src (context, th) =
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/generic_target.ML
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -20,7 +20,6 @@
   val thy_decl: T
   val thy_load: T
   val thy_load_files: string list -> T
-  val thy_script: T
   val thy_goal: T
   val qed: T
   val qed_script: T
@@ -101,7 +100,6 @@
 val thy_decl = kind "thy_decl";
 val thy_load = kind "thy_load";
 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
-val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
 val qed_script = kind "qed_script";
@@ -123,7 +121,7 @@
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
+    thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
@@ -249,7 +247,7 @@
 
 val is_theory = command_category
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal];
+    thy_load, thy_decl, thy_goal];
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Mar 14 17:32:11 2014 +0100
@@ -22,7 +22,6 @@
   val THY_HEADING4 = "thy_heading4"
   val THY_DECL = "thy_decl"
   val THY_LOAD = "thy_load"
-  val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
   val QED_SCRIPT = "qed_script"
@@ -50,7 +49,7 @@
   val diag = Set(DIAG)
   val theory =
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-      THY_DECL, THY_SCRIPT, THY_GOAL)
+      THY_DECL, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
@@ -61,6 +60,5 @@
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
       PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
-  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/local_theory.ML
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/locale.ML
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -30,7 +30,6 @@
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
-  val facts_of: Proof.context -> Facts.T
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
@@ -53,9 +52,10 @@
   val transfer: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
-  val extern_fact: Proof.context -> string -> xstring
+  val facts_of: Proof.context -> Facts.T
+  val facts_of_fact: Proof.context -> string -> Facts.T
+  val markup_extern_fact: Proof.context -> string -> Markup.T * xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
-  val markup_fact: Proof.context -> string -> Markup.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
   val read_class: Proof.context -> string -> class
@@ -120,6 +120,7 @@
     (term list list * (Proof.context -> Proof.context)) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
+  val get_fact_generic: Context.generic -> Facts.ref -> thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
@@ -209,7 +210,7 @@
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
-    facts: Facts.T,              (*local facts*)
+    facts: Facts.T,              (*local facts, based on initial global facts*)
     cases: cases};               (*named case contexts: case, is_proper, running index*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
@@ -219,9 +220,12 @@
 (
   type T = data;
   fun init thy =
-    make_data (mode_default, Local_Syntax.init thy,
-      (Sign.tsig_of thy, Sign.tsig_of thy),
-      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
+    make_data (mode_default,
+      Local_Syntax.init thy,
+      (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
+      (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+      Global_Theory.facts_of thy,
+      empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
@@ -274,7 +278,6 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_data;
-val facts_of = #facts o rep_data;
 val cases_of = #cases o rep_data;
 
 
@@ -334,31 +337,30 @@
   in (res, ctxt |> transfer thy') end;
 
 
-
-(** pretty printing **)
+(* hybrid facts *)
 
-(* extern *)
+val facts_of = #facts o rep_data;
 
-fun which_facts ctxt name =
+fun facts_of_fact ctxt name =
   let
     val local_facts = facts_of ctxt;
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
-    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
+    if Facts.defined local_facts name
     then local_facts else global_facts
   end;
 
-fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
-
-fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
+fun markup_extern_fact ctxt name =
+  Facts.markup_extern ctxt (facts_of_fact ctxt name) name;
 
 
-(* pretty *)
+
+(** pretty printing **)
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
-  Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
+  Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let
@@ -908,12 +910,22 @@
 end;
 
 
-(* get_thm(s) *)
+(* get facts *)
 
 local
 
-fun retrieve_thms pick ctxt (Facts.Fact s) =
+fun retrieve_global context =
+  Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
+
+fun retrieve_generic (context as Context.Proof ctxt) (xname, pos) =
+      if can (fn () => Facts.retrieve context (facts_of ctxt) (xname, Position.none)) ()
+      then Facts.retrieve context (facts_of ctxt) (xname, pos)
+      else retrieve_global context (xname, pos)
+  | retrieve_generic context arg = retrieve_global context arg;
+
+fun retrieve pick context (Facts.Fact s) =
       let
+        val ctxt = Context.the_proof context;
         val pos = Syntax.read_token_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
@@ -924,34 +936,27 @@
         fun prove_fact th =
           Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
         val results = map_filter (try prove_fact) (potential_facts ctxt prop');
-        val res =
+        val thm =
           (case distinct Thm.eq_thm_prop results of
-            [res] => res
+            [thm] => thm
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
-      in pick ("", Position.none) [res] end
-  | retrieve_thms pick ctxt xthmref =
+      in pick ("", Position.none) [thm] end
+  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
       let
-        val thy = theory_of ctxt;
-        val local_facts = facts_of ctxt;
-        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
-        val name = Facts.name_of_ref thmref;
-        val pos = Facts.pos_of_ref xthmref;
-        val thms =
-          if name = "" then [Thm.transfer thy Drule.dummy_thm]
-          else
-            (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME (_, ths) =>
-                (Context_Position.report ctxt pos
-                  (Name_Space.markup (Facts.space_of local_facts) name);
-                 map (Thm.transfer thy) (Facts.select thmref ths))
-            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
-      in pick (name, pos) thms end;
+        val thy = Context.theory_of context;
+        val (name, thms) =
+          (case xname of
+            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
+          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+          | _ => retrieve_generic context (xname, pos));
+      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
 
 in
 
-val get_fact = retrieve_thms (K I);
-val get_fact_single = retrieve_thms Facts.the_single;
+val get_fact_generic = retrieve (K I);
+val get_fact = retrieve (K I) o Context.Proof;
+val get_fact_single = retrieve Facts.the_single o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
@@ -1162,8 +1167,11 @@
       (Name_Space.del_table name cases, index)
   | update_case context is_proper (name, SOME c) (cases, index) =
       let
-        val (_, cases') = cases |> Name_Space.define context false
-          (Binding.make (name, Position.none), ((c, is_proper), index));
+        val binding =
+          Binding.make (name, Position.none)
+          |> not is_proper ? Binding.conceal;
+        val (_, cases') = cases
+          |> Name_Space.define context false (binding, ((c, is_proper), index));
         val index' = index + 1;
       in (cases', index') end;
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -590,11 +590,12 @@
 (* post-transition hooks *)
 
 local
-  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+  val hooks =
+    Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list);
 in
 
-fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = ! hooks;
+fun add_hook hook = Synchronized.change hooks (cons hook);
+fun get_hooks () = Synchronized.value hooks;
 
 end;
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -190,17 +190,18 @@
   in (thy, present, size text) end;
 
 
-(* document antiquotation *)
+(* antiquotations *)
 
-fun file_antiq strict ctxt (name, pos) =
+local
+
+fun check_path strict ctxt dir (name, pos) =
   let
     val _ = Context_Position.report ctxt pos Markup.language_path;
 
-    val dir = master_directory (Proof_Context.theory_of ctxt);
     val path = Path.append dir (Path.explode name)
       handle ERROR msg => error (msg ^ Position.here pos);
 
-    val _ = Context_Position.report ctxt pos (Markup.path name);
+    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
     val _ =
       if can Path.expand path andalso File.exists path then ()
       else
@@ -213,16 +214,30 @@
             Context_Position.if_visible ctxt Output.report
               (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
         end;
+  in path end;
+
+fun file_antiq strict ctxt (name, pos) =
+  let
+    val dir = master_directory (Proof_Context.theory_of ctxt);
+    val _ = check_path strict ctxt dir (name, pos);
   in
     space_explode "/" name
     |> map Thy_Output.verb_text
     |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
   end;
 
+in
+
 val _ = Theory.setup
-  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
     (file_antiq true o #context) #>
-  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
-    (file_antiq false o #context)));
+  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+    (file_antiq false o #context) #>
+  ML_Antiquotation.value (Binding.name "path")
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
+      let val path = check_path true ctxt Path.current arg
+      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
 
 end;
+
+end;
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -354,8 +354,9 @@
 
 fun nicer_shortest ctxt =
   let
-    val space = Facts.space_of (Proof_Context.facts_of ctxt);
-    val extern_shortest = Name_Space.extern_shortest ctxt space;
+    fun extern_shortest name =
+      Name_Space.extern_shortest ctxt
+        (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (extern_shortest x, i) (extern_shortest y, j)
@@ -454,7 +455,7 @@
         Facts.Named ((name, _), sel) => (name, sel)
       | Facts.Fact _ => raise Fail "Illegal literal fact");
   in
-    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
+    [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   end;
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/Tools/keywords.scala	Fri Mar 14 17:32:11 2014 +0100
@@ -25,7 +25,6 @@
     "thy_heading4" -> "theory-heading",
     "thy_load" -> "theory-decl",
     "thy_decl" -> "theory-decl",
-    "thy_script" -> "theory-script",
     "thy_goal" -> "theory-goal",
     "qed_script" -> "qed",
     "qed_block" -> "qed-block",
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/axclass.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -391,9 +391,9 @@
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
-    val (th', thy') =
-      Global_Theory.store_thm
-        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+    val binding =
+      Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
+    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
     val th'' = th'
       |> Thm.unconstrainT
       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -412,9 +412,9 @@
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
 
-    val (th', thy') =
-      Global_Theory.store_thm
-        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+    val binding =
+      Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
+    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/consts.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -10,6 +10,7 @@
   type T
   val eq_consts: T * T -> bool
   val change_base: bool -> T -> T
+  val change_ignore: T -> T
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
    {const_space: Name_Space.T,
@@ -69,6 +70,9 @@
 fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
   (Name_Space.change_base begin decls, constraints, rev_abbrevs));
 
+val change_ignore = map_consts (fn (decls, constraints, rev_abbrevs) =>
+  (Name_Space.change_ignore decls, constraints, rev_abbrevs));
+
 
 (* reverted abbrevs *)
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/facts.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -26,7 +26,9 @@
   val check: Context.generic -> T -> xstring * Position.T -> string
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
+  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
+  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: T list -> T -> (string * thm list) list
@@ -155,6 +157,7 @@
 
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
+fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
 
 val defined = is_some oo (Name_Space.lookup_key o facts_of);
 
@@ -164,6 +167,18 @@
   | SOME (_, Static ths) => SOME (true, ths)
   | SOME (_, Dynamic f) => SOME (false, f context));
 
+fun retrieve context facts (xname, pos) =
+  let
+    val name = check context facts (xname, pos);
+    val thms =
+      (case lookup context facts name of
+        SOME (static, thms) =>
+          (if static then ()
+           else Context_Position.report_generic context pos (Markup.dynamic_fact name);
+           thms)
+      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
+  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+
 fun fold_static f =
   Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
 
@@ -195,7 +210,10 @@
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
     val facts' = Name_Space.merge_tables (facts1, facts2);
-    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
+    val props' =
+      if Net.is_empty props2 then props1
+      else if Net.is_empty props1 then props2
+      else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
   in make_facts facts' props' end;
 
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/global_theory.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -11,7 +11,6 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val all_thms_of: theory -> (string * thm) list
@@ -64,31 +63,13 @@
 fun hide_fact fully name = Data.map (Facts.hide fully name);
 
 
-(** retrieve theorems **)
-
-fun get_fact context thy xthmref =
-  let
-    val facts = facts_of thy;
-    val xname = Facts.name_of_ref xthmref;
-    val pos = Facts.pos_of_ref xthmref;
+(* retrieve theorems *)
 
-    val name =
-      (case intern_fact thy xname of
-        "_" => "Pure.asm_rl"
-      | name => name);
-    val res = Facts.lookup context facts name;
-  in
-    (case res of
-      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
-    | SOME (static, ths) =>
-        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
-         if static then ()
-         else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-         Facts.select xthmref (map (Thm.transfer thy) ths)))
-  end;
+fun get_thms thy xname =
+  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
 
-fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
-fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
+fun get_thm thy xname =
+  Facts.the_single (xname, Position.none) (get_thms thy xname);
 
 fun all_thms_of thy =
   Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/net.ML
--- a/src/Pure/net.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/net.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -253,7 +253,7 @@
       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
 
 fun merge eq (net1, net2) =
-  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
+  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-canonical merge order!?! *)
 
 fun content net = map #2 (dest net);
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Pure/type.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -26,6 +26,7 @@
     types: decl Name_Space.table,
     log_types: string list}
   val change_base: bool -> tsig -> tsig
+  val change_ignore: tsig -> tsig
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
@@ -180,6 +181,9 @@
 fun change_base begin (TSig {classes, default, types, log_types}) =
   make_tsig (classes, default, Name_Space.change_base begin types, log_types);
 
+fun change_ignore (TSig {classes, default, types, log_types}) =
+  make_tsig (classes, default, Name_Space.change_ignore types, log_types);
+
 fun build_tsig (classes, default, types) =
   let
     val log_types =
diff -r 64eeda68e693 -r d94d6a9178b5 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -177,7 +177,7 @@
 
 local
 val (fromsym, fromabbr, tosym, toabbr) =
-  read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
+  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
 in
 val symbol_to_unicode = Symtab.lookup fromsym;
 val abbrev_to_unicode = Symtab.lookup fromabbr;
diff -r 64eeda68e693 -r d94d6a9178b5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 17:32:11 2014 +0100
@@ -53,7 +53,6 @@
     import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
-      Keyword.THY_SCRIPT -> LABEL,
       Keyword.QED_SCRIPT -> DIGIT,
       Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
@@ -471,7 +470,8 @@
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
-            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
+            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+            Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
diff -r 64eeda68e693 -r d94d6a9178b5 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/Tools/misc_legacy.ML	Fri Mar 14 17:32:11 2014 +0100
@@ -246,10 +246,11 @@
 val char_vec = Vector.tabulate (62, gensym_char);
 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
 
-val gensym_seed = Unsynchronized.ref (0: int);
+val gensym_seed = Synchronized.var "gensym_seed" (0: int);
 
 in
-  fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
+  fun gensym pre =
+    Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
 end;
 
 
diff -r 64eeda68e693 -r d94d6a9178b5 src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy	Fri Mar 14 17:32:11 2014 +0100
@@ -14,8 +14,7 @@
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
 keywords
-  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
-  "inductive_cases" :: thy_script and
+  "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   "elimination" "induction" "case_eqns" "recursor_eqns"
 begin