merged
authorwenzelm
Fri Mar 14 17:32:11 2014 +0100 (2014-03-14)
changeset 56148d94d6a9178b5
parent 56132 64eeda68e693
parent 56147 9589605bcf41
child 56149 ede82d6e0abd
merged
NEWS
etc/isar-keywords.el
     1.1 --- a/NEWS	Fri Mar 14 12:09:51 2014 +0100
     1.2 +++ b/NEWS	Fri Mar 14 17:32:11 2014 +0100
     1.3 @@ -460,6 +460,12 @@
     1.4  * ML antiquotation @{here} refers to its source position, which is
     1.5  occasionally useful for experimentation and diagnostic purposes.
     1.6  
     1.7 +* ML antiquotation @{path} produces a Path.T value, similarly to
     1.8 +Path.explode, but with compile-time check against the file-system and
     1.9 +some PIDE markup.  Note that unlike theory source, ML does not have a
    1.10 +well-defined master directory, so an absolute symbolic path
    1.11 +specification is usually required, e.g. "~~/src/HOL".
    1.12 +
    1.13  
    1.14  *** System ***
    1.15  
     2.1 --- a/etc/isar-keywords-ZF.el	Fri Mar 14 12:09:51 2014 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Mar 14 17:32:11 2014 +0100
     2.3 @@ -367,6 +367,7 @@
     2.4      "hide_fact"
     2.5      "hide_type"
     2.6      "inductive"
     2.7 +    "inductive_cases"
     2.8      "instantiation"
     2.9      "judgment"
    2.10      "lemmas"
    2.11 @@ -404,7 +405,7 @@
    2.12      "typedecl"))
    2.13  
    2.14  (defconst isar-keywords-theory-script
    2.15 -  '("inductive_cases"))
    2.16 +  '())
    2.17  
    2.18  (defconst isar-keywords-theory-goal
    2.19    '("corollary"
     3.1 --- a/etc/isar-keywords.el	Fri Mar 14 12:09:51 2014 +0100
     3.2 +++ b/etc/isar-keywords.el	Fri Mar 14 17:32:11 2014 +0100
     3.3 @@ -532,7 +532,9 @@
     3.4      "import_tptp"
     3.5      "import_type_map"
     3.6      "inductive"
     3.7 +    "inductive_cases"
     3.8      "inductive_set"
     3.9 +    "inductive_simps"
    3.10      "instantiation"
    3.11      "judgment"
    3.12      "lemmas"
    3.13 @@ -592,8 +594,7 @@
    3.14      "typedecl"))
    3.15  
    3.16  (defconst isar-keywords-theory-script
    3.17 -  '("inductive_cases"
    3.18 -    "inductive_simps"))
    3.19 +  '())
    3.20  
    3.21  (defconst isar-keywords-theory-goal
    3.22    '("ax_specification"
     4.1 --- a/src/Doc/antiquote_setup.ML	Fri Mar 14 12:09:51 2014 +0100
     4.2 +++ b/src/Doc/antiquote_setup.ML	Fri Mar 14 17:32:11 2014 +0100
     4.3 @@ -166,12 +166,12 @@
     4.4    | parse_named _ _ = [];
     4.5  
     4.6  val jedit_actions =
     4.7 -  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
     4.8 +  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     4.9      XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    4.10    | _ => []);
    4.11  
    4.12  val jedit_dockables =
    4.13 -  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
    4.14 +  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
    4.15      XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    4.16    | _ => []);
    4.17  
     5.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 14 12:09:51 2014 +0100
     5.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 14 17:32:11 2014 +0100
     5.3 @@ -448,8 +448,8 @@
     5.4    by unfold_locales  (* subsumed, thm int2.assoc not generated *)
     5.5  
     5.6  ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
     5.7 -    error "thm int2.assoc was generated")
     5.8 -  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
     5.9 +    raise Fail "thm int2.assoc was generated")
    5.10 +  handle ERROR _ => ([]:thm list); *}
    5.11  
    5.12  thm int.lone int.right.rone
    5.13    (* the latter comes through the sublocale relation *)
    5.14 @@ -782,8 +782,8 @@
    5.15  context container begin
    5.16  ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
    5.17    val _ = Proof_Context.get_thms context "private.true" in generic end);
    5.18 -  error "thm private.true was persisted")
    5.19 -  handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
    5.20 +  raise Fail "thm private.true was persisted")
    5.21 +  handle ERROR _ => ([]:thm list); *}
    5.22  thm true_copy
    5.23  end
    5.24  
     6.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Mar 14 12:09:51 2014 +0100
     6.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Mar 14 17:32:11 2014 +0100
     6.3 @@ -456,7 +456,7 @@
     6.4  text {*Usually, if this rule causes a failed congruence proof error,
     6.5    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
     6.6    Adding @{thm [source] Pi_def} to the simpset is often useful.
     6.7 -  For this reason, @{thm [source] comm_monoid.finprod_cong}
     6.8 +  For this reason, @{thm [source] finprod_cong}
     6.9    is not added to the simpset by default.
    6.10  *}
    6.11  
     7.1 --- a/src/HOL/Inductive.thy	Fri Mar 14 12:09:51 2014 +0100
     7.2 +++ b/src/HOL/Inductive.thy	Fri Mar 14 17:32:11 2014 +0100
     7.3 @@ -7,8 +7,8 @@
     7.4  theory Inductive
     7.5  imports Complete_Lattices Ctr_Sugar
     7.6  keywords
     7.7 -  "inductive" "coinductive" :: thy_decl and
     7.8 -  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
     7.9 +  "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
    7.10 +  "monos" and
    7.11    "print_inductives" :: diag and
    7.12    "rep_datatype" :: thy_goal and
    7.13    "primrec" :: thy_decl
     8.1 --- a/src/HOL/Lattices_Big.thy	Fri Mar 14 12:09:51 2014 +0100
     8.2 +++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 17:32:11 2014 +0100
     8.3 @@ -640,6 +640,11 @@
     8.4    shows "Max M \<le> Max N"
     8.5    using assms by (fact Max.antimono)
     8.6  
     8.7 +end
     8.8 +
     8.9 +context linorder  (* FIXME *)
    8.10 +begin
    8.11 +
    8.12  lemma mono_Min_commute:
    8.13    assumes "mono f"
    8.14    assumes "finite A" and "A \<noteq> {}"
     9.1 --- a/src/HOL/Library/refute.ML	Fri Mar 14 12:09:51 2014 +0100
     9.2 +++ b/src/HOL/Library/refute.ML	Fri Mar 14 17:32:11 2014 +0100
     9.3 @@ -1073,7 +1073,7 @@
     9.4                handle Option.Option =>
     9.5                       error ("Unknown SAT solver: " ^ quote satsolver ^
     9.6                              ". Available solvers: " ^
     9.7 -                            commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
     9.8 +                            commas (map (quote o fst) (SatSolver.get_solvers ())) ^ ".")
     9.9            in
    9.10              Output.urgent_message "Invoking SAT solver...";
    9.11              (case solver fm of
    10.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Mar 14 12:09:51 2014 +0100
    10.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Mar 14 17:32:11 2014 +0100
    10.3 @@ -37,7 +37,7 @@
    10.4  
    10.5  ML {*
    10.6  fun mutation_testing_of (name, thy) =
    10.7 -  (MutabelleExtra.random_seed := 1.0;
    10.8 +  (MutabelleExtra.init_random 1.0;
    10.9    MutabelleExtra.thms_of false thy
   10.10    |> MutabelleExtra.take_random 200
   10.11    |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
   10.12 @@ -50,7 +50,7 @@
   10.13  (*
   10.14  ML {*
   10.15  
   10.16 -      MutabelleExtra.random_seed := 1.0;
   10.17 +      MutabelleExtra.init_random 1.0;
   10.18        MutabelleExtra.thms_of true @{theory Complex_Main}
   10.19        |> MutabelleExtra.take_random 1000000
   10.20        |> (fn thms => List.drop (thms, 1000))
    11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 14 12:09:51 2014 +0100
    11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 14 17:32:11 2014 +0100
    11.3 @@ -40,15 +40,12 @@
    11.4  val mutate_theorems_and_write_report :
    11.5    theory -> int * int -> mtd list -> thm list -> string -> unit
    11.6  
    11.7 -val random_seed : real Unsynchronized.ref
    11.8 +val init_random : real -> unit
    11.9  end;
   11.10  
   11.11  structure MutabelleExtra : MUTABELLE_EXTRA =
   11.12  struct
   11.13  
   11.14 -(* Own seed; can't rely on the Isabelle one to stay the same *)
   11.15 -val random_seed = Unsynchronized.ref 1.0;
   11.16 -
   11.17  (* Another Random engine *)
   11.18  
   11.19  exception RANDOM;
   11.20 @@ -56,13 +53,20 @@
   11.21  fun rmod x y = x - y * Real.realFloor (x / y);
   11.22  
   11.23  local
   11.24 +  (* Own seed; can't rely on the Isabelle one to stay the same *)
   11.25 +  val random_seed = Synchronized.var "random_seed" 1.0;
   11.26 +
   11.27    val a = 16807.0;
   11.28    val m = 2147483647.0;
   11.29  in
   11.30  
   11.31 -fun random () = CRITICAL (fn () =>
   11.32 -  let val r = rmod (a * ! random_seed) m
   11.33 -  in (random_seed := r; r) end);
   11.34 +fun init_random r = Synchronized.change random_seed (K r);
   11.35 +
   11.36 +fun random () =
   11.37 +  Synchronized.change_result random_seed
   11.38 +    (fn s =>
   11.39 +      let val r = rmod (a * s) m
   11.40 +      in (r, r) end);
   11.41  
   11.42  end;
   11.43  
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 14 12:09:51 2014 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Mar 14 17:32:11 2014 +0100
    12.3 @@ -573,7 +573,7 @@
    12.4        let
    12.5          (* use the first ML solver (to avoid startup overhead) *)
    12.6          val (ml_solvers, nonml_solvers) =
    12.7 -          !SatSolver.solvers
    12.8 +          SatSolver.get_solvers ()
    12.9            |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
   12.10          val res =
   12.11            if null nonml_solvers then
    13.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 14 12:09:51 2014 +0100
    13.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 14 17:32:11 2014 +0100
    13.3 @@ -200,10 +200,10 @@
    13.4  (** invocation of Haskell interpreter **)
    13.5  
    13.6  val narrowing_engine =
    13.7 -  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
    13.8 +  File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
    13.9  
   13.10  val pnf_narrowing_engine =
   13.11 -  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   13.12 +  File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
   13.13  
   13.14  fun exec verbose code =
   13.15    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 12:09:51 2014 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 17:32:11 2014 +0100
    14.3 @@ -459,7 +459,7 @@
    14.4        else
    14.5          is_too_complex
    14.6      val local_facts = Proof_Context.facts_of ctxt
    14.7 -    val named_locals = local_facts |> Facts.dest_static []
    14.8 +    val named_locals = local_facts |> Facts.dest_static [global_facts]
    14.9      val assms = Assumption.all_assms_of ctxt
   14.10      fun is_good_unnamed_local th =
   14.11        not (Thm.has_name_hint th) andalso
    15.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Mar 14 12:09:51 2014 +0100
    15.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 14 17:32:11 2014 +0100
    15.3 @@ -42,7 +42,7 @@
    15.4    val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
    15.5  
    15.6    (* generic solver interface *)
    15.7 -  val solvers       : (string * solver) list Unsynchronized.ref
    15.8 +  val get_solvers   : unit -> (string * solver) list
    15.9    val add_solver    : string * solver -> unit
   15.10    val invoke_solver : string -> solver  (* exception Option *)
   15.11  end;
   15.12 @@ -348,22 +348,24 @@
   15.13    end;
   15.14  
   15.15  (* ------------------------------------------------------------------------- *)
   15.16 -(* solvers: a (reference to a) table of all registered SAT solvers           *)
   15.17 +(* solvers: a table of all registered SAT solvers                            *)
   15.18  (* ------------------------------------------------------------------------- *)
   15.19  
   15.20 -  val solvers = Unsynchronized.ref ([] : (string * solver) list);
   15.21 +  val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
   15.22 +
   15.23 +  fun get_solvers () = Synchronized.value solvers;
   15.24  
   15.25  (* ------------------------------------------------------------------------- *)
   15.26  (* add_solver: updates 'solvers' by adding a new solver                      *)
   15.27  (* ------------------------------------------------------------------------- *)
   15.28  
   15.29 -    fun add_solver (name, new_solver) = CRITICAL (fn () =>
   15.30 +  fun add_solver (name, new_solver) =
   15.31 +    Synchronized.change solvers (fn the_solvers =>
   15.32        let
   15.33 -        val the_solvers = !solvers;
   15.34          val _ = if AList.defined (op =) the_solvers name
   15.35            then warning ("SAT solver " ^ quote name ^ " was defined before")
   15.36            else ();
   15.37 -      in solvers := AList.update (op =) (name, new_solver) the_solvers end);
   15.38 +      in AList.update (op =) (name, new_solver) the_solvers end);
   15.39  
   15.40  (* ------------------------------------------------------------------------- *)
   15.41  (* invoke_solver: returns the solver associated with the given 'name'        *)
   15.42 @@ -372,7 +374,7 @@
   15.43  (* ------------------------------------------------------------------------- *)
   15.44  
   15.45    fun invoke_solver name =
   15.46 -    (the o AList.lookup (op =) (!solvers)) name;
   15.47 +    the (AList.lookup (op =) (get_solvers ()) name);
   15.48  
   15.49  end;  (* SatSolver *)
   15.50  
   15.51 @@ -521,7 +523,7 @@
   15.52            handle SatSolver.NOT_CONFIGURED => loop solvers
   15.53        )
   15.54    in
   15.55 -    loop (!SatSolver.solvers)
   15.56 +    loop (SatSolver.get_solvers ())
   15.57    end
   15.58  in
   15.59    SatSolver.add_solver ("auto", auto_solver)
    16.1 --- a/src/Pure/General/change_table.ML	Fri Mar 14 12:09:51 2014 +0100
    16.2 +++ b/src/Pure/General/change_table.ML	Fri Mar 14 17:32:11 2014 +0100
    16.3 @@ -17,6 +17,7 @@
    16.4    val empty: 'a T
    16.5    val is_empty: 'a T -> bool
    16.6    val change_base: bool -> 'a T -> 'a T
    16.7 +  val change_ignore: 'a T -> 'a T
    16.8    val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
    16.9    val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   16.10    val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
   16.11 @@ -43,35 +44,42 @@
   16.12  
   16.13  (* optional change *)
   16.14  
   16.15 -datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set};
   16.16 +datatype change =
   16.17 +  No_Change | Change of {base: serial, depth: int, changes: Table.set option};
   16.18  
   16.19  fun make_change base depth changes =
   16.20    Change {base = base, depth = depth, changes = changes};
   16.21  
   16.22 +fun ignore_change (Change {base, depth, changes = SOME _}) =
   16.23 +      make_change base depth NONE
   16.24 +  | ignore_change change = change;
   16.25 +
   16.26 +fun update_change key (Change {base, depth, changes = SOME ch}) =
   16.27 +      make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
   16.28 +  | update_change _ change = change;
   16.29 +
   16.30  fun base_change true No_Change =
   16.31 -      make_change (serial ()) 0 Table.empty
   16.32 +      make_change (serial ()) 0 (SOME Table.empty)
   16.33    | base_change true (Change {base, depth, changes}) =
   16.34        make_change base (depth + 1) changes
   16.35    | base_change false (Change {base, depth, changes}) =
   16.36        if depth = 0 then No_Change else make_change base (depth - 1) changes
   16.37 -  | base_change false No_Change = raise Fail "Unbalanced block structure of change table";
   16.38 +  | base_change false No_Change = raise Fail "Unbalanced change structure";
   16.39  
   16.40 -fun update_change _ No_Change = No_Change
   16.41 -  | update_change key (Change {base, depth, changes}) =
   16.42 -      make_change base depth (Table.insert (K true) (key, ()) changes);
   16.43 -
   16.44 -fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
   16.45 +fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure";
   16.46  
   16.47  fun merge_change (No_Change, No_Change) = NONE
   16.48    | merge_change (Change change1, Change change2) =
   16.49        let
   16.50          val {base = base1, depth = depth1, changes = changes1} = change1;
   16.51          val {base = base2, depth = depth2, changes = changes2} = change2;
   16.52 -      in
   16.53 -        if base1 = base2 andalso depth1 = depth2 then
   16.54 -          SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
   16.55 -        else cannot_merge ()
   16.56 -      end
   16.57 +        val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge ();
   16.58 +        val (swapped, ch2) =
   16.59 +          (case (changes1, changes2) of
   16.60 +            (_, SOME ch2) => (false, ch2)
   16.61 +          | (SOME ch1, _) => (true, ch1)
   16.62 +          | _ => cannot_merge ());
   16.63 +      in SOME (swapped, ch2, make_change base1 depth1 NONE) end
   16.64    | merge_change _ = cannot_merge ();
   16.65  
   16.66  
   16.67 @@ -90,6 +98,7 @@
   16.68  fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
   16.69  
   16.70  fun change_base begin = (map_change_table o apfst) (base_change begin);
   16.71 +fun change_ignore arg = (map_change_table o apfst) ignore_change arg;
   16.72  
   16.73  
   16.74  (* join and merge *)
   16.75 @@ -105,20 +114,21 @@
   16.76      else
   16.77        (case merge_change (change1, change2) of
   16.78          NONE => make_change_table (No_Change, Table.join f (table1, table2))
   16.79 -      | SOME (changes2, change') =>
   16.80 +      | SOME (swapped, ch2, change') =>
   16.81            let
   16.82 -            fun update key table =
   16.83 -              (case Table.lookup table2 key of
   16.84 -                NONE => table
   16.85 +            fun maybe_swap (x, y) = if swapped then (y, x) else (x, y);
   16.86 +            val (tab1, tab2) = maybe_swap (table1, table2);
   16.87 +            fun update key tab =
   16.88 +              (case Table.lookup tab2 key of
   16.89 +                NONE => tab
   16.90                | SOME y =>
   16.91 -                  (case Table.lookup table key of
   16.92 -                    NONE => Table.update (key, y) table
   16.93 +                  (case Table.lookup tab key of
   16.94 +                    NONE => Table.update (key, y) tab
   16.95                    | SOME x =>
   16.96 -                      (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
   16.97 -                        NONE => table
   16.98 -                      | SOME z => Table.update (key, z) table)));
   16.99 -            val table' = Table.fold (update o #1) changes2 table1;
  16.100 -          in make_change_table (change', table') end)
  16.101 +                      (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
  16.102 +                        NONE => tab
  16.103 +                      | SOME z => Table.update (key, z) tab)));
  16.104 +          in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
  16.105    end;
  16.106  
  16.107  fun merge eq =
    17.1 --- a/src/Pure/General/name_space.ML	Fri Mar 14 12:09:51 2014 +0100
    17.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 14 17:32:11 2014 +0100
    17.3 @@ -56,6 +56,7 @@
    17.4    val declare: Context.generic -> bool -> binding -> T -> string * T
    17.5    type 'a table
    17.6    val change_base: bool -> 'a table -> 'a table
    17.7 +  val change_ignore: 'a table -> 'a table
    17.8    val space_of_table: 'a table -> T
    17.9    val check_reports: Context.generic -> 'a table ->
   17.10      xstring * Position.T list -> (string * Position.report list) * 'a
   17.11 @@ -123,6 +124,9 @@
   17.12  fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
   17.13    (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
   17.14  
   17.15 +val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
   17.16 +  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
   17.17 +
   17.18  fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
   17.19    (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
   17.20  
   17.21 @@ -474,6 +478,9 @@
   17.22  fun change_base begin (Table (space, tab)) =
   17.23    Table (change_base_space begin space, Change_Table.change_base begin tab);
   17.24  
   17.25 +fun change_ignore (Table (space, tab)) =
   17.26 +  Table (change_ignore_space space, Change_Table.change_ignore tab);
   17.27 +
   17.28  fun space_of_table (Table (space, _)) = space;
   17.29  
   17.30  fun check_reports context (Table (space, tab)) (xname, ps) =
    18.1 --- a/src/Pure/General/path.ML	Fri Mar 14 12:09:51 2014 +0100
    18.2 +++ b/src/Pure/General/path.ML	Fri Mar 14 17:32:11 2014 +0100
    18.3 @@ -30,6 +30,7 @@
    18.4    val ext: string -> T -> T
    18.5    val split_ext: T -> T * string
    18.6    val expand: T -> T
    18.7 +  val smart_implode: T -> string
    18.8    val position: T -> Position.T
    18.9  end;
   18.10  
   18.11 @@ -194,21 +195,26 @@
   18.12  val expand = rep #> maps eval #> norm #> Path;
   18.13  
   18.14  
   18.15 -(* source position -- with smart replacement of ISABELLE_HOME *)
   18.16 +(* smart implode *)
   18.17  
   18.18 -val isabelle_home = explode_path "~~";
   18.19 -
   18.20 -fun position path =
   18.21 +fun smart_implode path =
   18.22    let
   18.23 -    val s = implode_path path;
   18.24 -    val prfx = implode_path (expand isabelle_home) ^ "/";
   18.25 +    val full_name = implode_path (expand path);
   18.26 +    fun fold_path a =
   18.27 +      let val b = implode_path (expand (explode_path a)) in
   18.28 +        if full_name = b then SOME a
   18.29 +        else
   18.30 +          (case try (unprefix (b ^ "/")) full_name of
   18.31 +            SOME name => SOME (a ^ "/" ^ name)
   18.32 +          | NONE => NONE)
   18.33 +      end;
   18.34    in
   18.35 -    Position.file
   18.36 -      (case try (unprefix prfx) s of
   18.37 -        NONE => s
   18.38 -      | SOME s' => "~~/" ^ s')
   18.39 +    (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
   18.40 +      SOME name => name
   18.41 +    | NONE => implode_path path)
   18.42    end;
   18.43  
   18.44 +val position = Position.file o smart_implode;
   18.45  
   18.46  (*final declarations of this structure!*)
   18.47  val implode = implode_path;
    19.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 14 12:09:51 2014 +0100
    19.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 14 17:32:11 2014 +0100
    19.3 @@ -213,7 +213,7 @@
    19.4  
    19.5  fun gen_thm pick = Scan.depend (fn context =>
    19.6    let
    19.7 -    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
    19.8 +    val get = Proof_Context.get_fact_generic context;
    19.9      val get_fact = get o Facts.Fact;
   19.10      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   19.11    in
   19.12 @@ -249,6 +249,8 @@
   19.13  
   19.14  (** partial evaluation -- observing rule/declaration/mixed attributes **)
   19.15  
   19.16 +(*NB: result length may change due to rearrangement of symbolic expression*)
   19.17 +
   19.18  local
   19.19  
   19.20  fun apply_att src (context, th) =
    21.1 --- a/src/Pure/Isar/keyword.ML	Fri Mar 14 12:09:51 2014 +0100
    21.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 14 17:32:11 2014 +0100
    21.3 @@ -20,7 +20,6 @@
    21.4    val thy_decl: T
    21.5    val thy_load: T
    21.6    val thy_load_files: string list -> T
    21.7 -  val thy_script: T
    21.8    val thy_goal: T
    21.9    val qed: T
   21.10    val qed_script: T
   21.11 @@ -101,7 +100,6 @@
   21.12  val thy_decl = kind "thy_decl";
   21.13  val thy_load = kind "thy_load";
   21.14  fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
   21.15 -val thy_script = kind "thy_script";
   21.16  val thy_goal = kind "thy_goal";
   21.17  val qed = kind "qed";
   21.18  val qed_script = kind "qed_script";
   21.19 @@ -123,7 +121,7 @@
   21.20  
   21.21  val kinds =
   21.22    [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
   21.23 -    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
   21.24 +    thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
   21.25      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
   21.26      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
   21.27  
   21.28 @@ -249,7 +247,7 @@
   21.29  
   21.30  val is_theory = command_category
   21.31    [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
   21.32 -    thy_load, thy_decl, thy_script, thy_goal];
   21.33 +    thy_load, thy_decl, thy_goal];
   21.34  
   21.35  val is_proof = command_category
   21.36    [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    22.1 --- a/src/Pure/Isar/keyword.scala	Fri Mar 14 12:09:51 2014 +0100
    22.2 +++ b/src/Pure/Isar/keyword.scala	Fri Mar 14 17:32:11 2014 +0100
    22.3 @@ -22,7 +22,6 @@
    22.4    val THY_HEADING4 = "thy_heading4"
    22.5    val THY_DECL = "thy_decl"
    22.6    val THY_LOAD = "thy_load"
    22.7 -  val THY_SCRIPT = "thy_script"
    22.8    val THY_GOAL = "thy_goal"
    22.9    val QED = "qed"
   22.10    val QED_SCRIPT = "qed_script"
   22.11 @@ -50,7 +49,7 @@
   22.12    val diag = Set(DIAG)
   22.13    val theory =
   22.14      Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
   22.15 -      THY_DECL, THY_SCRIPT, THY_GOAL)
   22.16 +      THY_DECL, THY_GOAL)
   22.17    val theory1 = Set(THY_BEGIN, THY_END)
   22.18    val theory2 = Set(THY_DECL, THY_GOAL)
   22.19    val proof =
   22.20 @@ -61,6 +60,5 @@
   22.21      Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
   22.22        PRF_CHAIN, PRF_DECL)
   22.23    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   22.24 -  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
   22.25  }
   22.26  
    25.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 12:09:51 2014 +0100
    25.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 17:32:11 2014 +0100
    25.3 @@ -30,7 +30,6 @@
    25.4    val consts_of: Proof.context -> Consts.T
    25.5    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
    25.6    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    25.7 -  val facts_of: Proof.context -> Facts.T
    25.8    val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
    25.9    val naming_of: Proof.context -> Name_Space.naming
   25.10    val restore_naming: Proof.context -> Proof.context -> Proof.context
   25.11 @@ -53,9 +52,10 @@
   25.12    val transfer: theory -> Proof.context -> Proof.context
   25.13    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   25.14    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   25.15 -  val extern_fact: Proof.context -> string -> xstring
   25.16 +  val facts_of: Proof.context -> Facts.T
   25.17 +  val facts_of_fact: Proof.context -> string -> Facts.T
   25.18 +  val markup_extern_fact: Proof.context -> string -> Markup.T * xstring
   25.19    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   25.20 -  val markup_fact: Proof.context -> string -> Markup.T
   25.21    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   25.22    val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
   25.23    val read_class: Proof.context -> string -> class
   25.24 @@ -120,6 +120,7 @@
   25.25      (term list list * (Proof.context -> Proof.context)) * Proof.context
   25.26    val fact_tac: Proof.context -> thm list -> int -> tactic
   25.27    val some_fact_tac: Proof.context -> int -> tactic
   25.28 +  val get_fact_generic: Context.generic -> Facts.ref -> thm list
   25.29    val get_fact: Proof.context -> Facts.ref -> thm list
   25.30    val get_fact_single: Proof.context -> Facts.ref -> thm
   25.31    val get_thms: Proof.context -> xstring -> thm list
   25.32 @@ -209,7 +210,7 @@
   25.33      syntax: Local_Syntax.T,      (*local syntax*)
   25.34      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
   25.35      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
   25.36 -    facts: Facts.T,              (*local facts*)
   25.37 +    facts: Facts.T,              (*local facts, based on initial global facts*)
   25.38      cases: cases};               (*named case contexts: case, is_proper, running index*)
   25.39  
   25.40  fun make_data (mode, syntax, tsig, consts, facts, cases) =
   25.41 @@ -219,9 +220,12 @@
   25.42  (
   25.43    type T = data;
   25.44    fun init thy =
   25.45 -    make_data (mode_default, Local_Syntax.init thy,
   25.46 -      (Sign.tsig_of thy, Sign.tsig_of thy),
   25.47 -      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
   25.48 +    make_data (mode_default,
   25.49 +      Local_Syntax.init thy,
   25.50 +      (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
   25.51 +      (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
   25.52 +      Global_Theory.facts_of thy,
   25.53 +      empty_cases);
   25.54  );
   25.55  
   25.56  fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
   25.57 @@ -274,7 +278,6 @@
   25.58  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
   25.59  
   25.60  val consts_of = #1 o #consts o rep_data;
   25.61 -val facts_of = #facts o rep_data;
   25.62  val cases_of = #cases o rep_data;
   25.63  
   25.64  
   25.65 @@ -334,31 +337,30 @@
   25.66    in (res, ctxt |> transfer thy') end;
   25.67  
   25.68  
   25.69 -
   25.70 -(** pretty printing **)
   25.71 +(* hybrid facts *)
   25.72  
   25.73 -(* extern *)
   25.74 +val facts_of = #facts o rep_data;
   25.75  
   25.76 -fun which_facts ctxt name =
   25.77 +fun facts_of_fact ctxt name =
   25.78    let
   25.79      val local_facts = facts_of ctxt;
   25.80      val global_facts = Global_Theory.facts_of (theory_of ctxt);
   25.81    in
   25.82 -    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
   25.83 +    if Facts.defined local_facts name
   25.84      then local_facts else global_facts
   25.85    end;
   25.86  
   25.87 -fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
   25.88 -
   25.89 -fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
   25.90 +fun markup_extern_fact ctxt name =
   25.91 +  Facts.markup_extern ctxt (facts_of_fact ctxt name) name;
   25.92  
   25.93  
   25.94 -(* pretty *)
   25.95 +
   25.96 +(** pretty printing **)
   25.97  
   25.98  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
   25.99  
  25.100  fun pretty_fact_name ctxt a =
  25.101 -  Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
  25.102 +  Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"];
  25.103  
  25.104  fun pretty_fact ctxt =
  25.105    let
  25.106 @@ -908,12 +910,22 @@
  25.107  end;
  25.108  
  25.109  
  25.110 -(* get_thm(s) *)
  25.111 +(* get facts *)
  25.112  
  25.113  local
  25.114  
  25.115 -fun retrieve_thms pick ctxt (Facts.Fact s) =
  25.116 +fun retrieve_global context =
  25.117 +  Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
  25.118 +
  25.119 +fun retrieve_generic (context as Context.Proof ctxt) (xname, pos) =
  25.120 +      if can (fn () => Facts.retrieve context (facts_of ctxt) (xname, Position.none)) ()
  25.121 +      then Facts.retrieve context (facts_of ctxt) (xname, pos)
  25.122 +      else retrieve_global context (xname, pos)
  25.123 +  | retrieve_generic context arg = retrieve_global context arg;
  25.124 +
  25.125 +fun retrieve pick context (Facts.Fact s) =
  25.126        let
  25.127 +        val ctxt = Context.the_proof context;
  25.128          val pos = Syntax.read_token_pos s;
  25.129          val prop =
  25.130            Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
  25.131 @@ -924,34 +936,27 @@
  25.132          fun prove_fact th =
  25.133            Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
  25.134          val results = map_filter (try prove_fact) (potential_facts ctxt prop');
  25.135 -        val res =
  25.136 +        val thm =
  25.137            (case distinct Thm.eq_thm_prop results of
  25.138 -            [res] => res
  25.139 +            [thm] => thm
  25.140            | [] => err "Failed to retrieve literal fact"
  25.141            | _ => err "Ambiguous specification of literal fact");
  25.142 -      in pick ("", Position.none) [res] end
  25.143 -  | retrieve_thms pick ctxt xthmref =
  25.144 +      in pick ("", Position.none) [thm] end
  25.145 +  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
  25.146        let
  25.147 -        val thy = theory_of ctxt;
  25.148 -        val local_facts = facts_of ctxt;
  25.149 -        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
  25.150 -        val name = Facts.name_of_ref thmref;
  25.151 -        val pos = Facts.pos_of_ref xthmref;
  25.152 -        val thms =
  25.153 -          if name = "" then [Thm.transfer thy Drule.dummy_thm]
  25.154 -          else
  25.155 -            (case Facts.lookup (Context.Proof ctxt) local_facts name of
  25.156 -              SOME (_, ths) =>
  25.157 -                (Context_Position.report ctxt pos
  25.158 -                  (Name_Space.markup (Facts.space_of local_facts) name);
  25.159 -                 map (Thm.transfer thy) (Facts.select thmref ths))
  25.160 -            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
  25.161 -      in pick (name, pos) thms end;
  25.162 +        val thy = Context.theory_of context;
  25.163 +        val (name, thms) =
  25.164 +          (case xname of
  25.165 +            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
  25.166 +          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
  25.167 +          | _ => retrieve_generic context (xname, pos));
  25.168 +      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
  25.169  
  25.170  in
  25.171  
  25.172 -val get_fact = retrieve_thms (K I);
  25.173 -val get_fact_single = retrieve_thms Facts.the_single;
  25.174 +val get_fact_generic = retrieve (K I);
  25.175 +val get_fact = retrieve (K I) o Context.Proof;
  25.176 +val get_fact_single = retrieve Facts.the_single o Context.Proof;
  25.177  
  25.178  fun get_thms ctxt = get_fact ctxt o Facts.named;
  25.179  fun get_thm ctxt = get_fact_single ctxt o Facts.named;
  25.180 @@ -1162,8 +1167,11 @@
  25.181        (Name_Space.del_table name cases, index)
  25.182    | update_case context is_proper (name, SOME c) (cases, index) =
  25.183        let
  25.184 -        val (_, cases') = cases |> Name_Space.define context false
  25.185 -          (Binding.make (name, Position.none), ((c, is_proper), index));
  25.186 +        val binding =
  25.187 +          Binding.make (name, Position.none)
  25.188 +          |> not is_proper ? Binding.conceal;
  25.189 +        val (_, cases') = cases
  25.190 +          |> Name_Space.define context false (binding, ((c, is_proper), index));
  25.191          val index' = index + 1;
  25.192        in (cases', index') end;
  25.193  
    26.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 14 12:09:51 2014 +0100
    26.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 14 17:32:11 2014 +0100
    26.3 @@ -590,11 +590,12 @@
    26.4  (* post-transition hooks *)
    26.5  
    26.6  local
    26.7 -  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
    26.8 +  val hooks =
    26.9 +    Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list);
   26.10  in
   26.11  
   26.12 -fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
   26.13 -fun get_hooks () = ! hooks;
   26.14 +fun add_hook hook = Synchronized.change hooks (cons hook);
   26.15 +fun get_hooks () = Synchronized.value hooks;
   26.16  
   26.17  end;
   26.18  
    27.1 --- a/src/Pure/Thy/thy_load.ML	Fri Mar 14 12:09:51 2014 +0100
    27.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Mar 14 17:32:11 2014 +0100
    27.3 @@ -190,17 +190,18 @@
    27.4    in (thy, present, size text) end;
    27.5  
    27.6  
    27.7 -(* document antiquotation *)
    27.8 +(* antiquotations *)
    27.9  
   27.10 -fun file_antiq strict ctxt (name, pos) =
   27.11 +local
   27.12 +
   27.13 +fun check_path strict ctxt dir (name, pos) =
   27.14    let
   27.15      val _ = Context_Position.report ctxt pos Markup.language_path;
   27.16  
   27.17 -    val dir = master_directory (Proof_Context.theory_of ctxt);
   27.18      val path = Path.append dir (Path.explode name)
   27.19        handle ERROR msg => error (msg ^ Position.here pos);
   27.20  
   27.21 -    val _ = Context_Position.report ctxt pos (Markup.path name);
   27.22 +    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
   27.23      val _ =
   27.24        if can Path.expand path andalso File.exists path then ()
   27.25        else
   27.26 @@ -213,16 +214,30 @@
   27.27              Context_Position.if_visible ctxt Output.report
   27.28                (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
   27.29          end;
   27.30 +  in path end;
   27.31 +
   27.32 +fun file_antiq strict ctxt (name, pos) =
   27.33 +  let
   27.34 +    val dir = master_directory (Proof_Context.theory_of ctxt);
   27.35 +    val _ = check_path strict ctxt dir (name, pos);
   27.36    in
   27.37      space_explode "/" name
   27.38      |> map Thy_Output.verb_text
   27.39      |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
   27.40    end;
   27.41  
   27.42 +in
   27.43 +
   27.44  val _ = Theory.setup
   27.45 -  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
   27.46 + (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
   27.47      (file_antiq true o #context) #>
   27.48 -  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
   27.49 -    (file_antiq false o #context)));
   27.50 +  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
   27.51 +    (file_antiq false o #context) #>
   27.52 +  ML_Antiquotation.value (Binding.name "path")
   27.53 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
   27.54 +      let val path = check_path true ctxt Path.current arg
   27.55 +      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
   27.56  
   27.57  end;
   27.58 +
   27.59 +end;
    28.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Mar 14 12:09:51 2014 +0100
    28.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 17:32:11 2014 +0100
    28.3 @@ -354,8 +354,9 @@
    28.4  
    28.5  fun nicer_shortest ctxt =
    28.6    let
    28.7 -    val space = Facts.space_of (Proof_Context.facts_of ctxt);
    28.8 -    val extern_shortest = Name_Space.extern_shortest ctxt space;
    28.9 +    fun extern_shortest name =
   28.10 +      Name_Space.extern_shortest ctxt
   28.11 +        (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
   28.12  
   28.13      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   28.14            nicer_name (extern_shortest x, i) (extern_shortest y, j)
   28.15 @@ -454,7 +455,7 @@
   28.16          Facts.Named ((name, _), sel) => (name, sel)
   28.17        | Facts.Fact _ => raise Fail "Illegal literal fact");
   28.18    in
   28.19 -    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
   28.20 +    [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
   28.21        Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   28.22    end;
   28.23  
    29.1 --- a/src/Pure/Tools/keywords.scala	Fri Mar 14 12:09:51 2014 +0100
    29.2 +++ b/src/Pure/Tools/keywords.scala	Fri Mar 14 17:32:11 2014 +0100
    29.3 @@ -25,7 +25,6 @@
    29.4      "thy_heading4" -> "theory-heading",
    29.5      "thy_load" -> "theory-decl",
    29.6      "thy_decl" -> "theory-decl",
    29.7 -    "thy_script" -> "theory-script",
    29.8      "thy_goal" -> "theory-goal",
    29.9      "qed_script" -> "qed",
   29.10      "qed_block" -> "qed-block",
    30.1 --- a/src/Pure/axclass.ML	Fri Mar 14 12:09:51 2014 +0100
    30.2 +++ b/src/Pure/axclass.ML	Fri Mar 14 17:32:11 2014 +0100
    30.3 @@ -391,9 +391,9 @@
    30.4      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    30.5      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    30.6      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    30.7 -    val (th', thy') =
    30.8 -      Global_Theory.store_thm
    30.9 -        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
   30.10 +    val binding =
   30.11 +      Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
   30.12 +    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   30.13      val th'' = th'
   30.14        |> Thm.unconstrainT
   30.15        |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   30.16 @@ -412,9 +412,9 @@
   30.17      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   30.18      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   30.19  
   30.20 -    val (th', thy') =
   30.21 -      Global_Theory.store_thm
   30.22 -        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
   30.23 +    val binding =
   30.24 +      Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
   30.25 +    val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   30.26  
   30.27      val args = Name.invent_names Name.context Name.aT Ss;
   30.28      val T = Type (t, map TFree args);
    31.1 --- a/src/Pure/consts.ML	Fri Mar 14 12:09:51 2014 +0100
    31.2 +++ b/src/Pure/consts.ML	Fri Mar 14 17:32:11 2014 +0100
    31.3 @@ -10,6 +10,7 @@
    31.4    type T
    31.5    val eq_consts: T * T -> bool
    31.6    val change_base: bool -> T -> T
    31.7 +  val change_ignore: T -> T
    31.8    val retrieve_abbrevs: T -> string list -> term -> (term * term) list
    31.9    val dest: T ->
   31.10     {const_space: Name_Space.T,
   31.11 @@ -69,6 +70,9 @@
   31.12  fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
   31.13    (Name_Space.change_base begin decls, constraints, rev_abbrevs));
   31.14  
   31.15 +val change_ignore = map_consts (fn (decls, constraints, rev_abbrevs) =>
   31.16 +  (Name_Space.change_ignore decls, constraints, rev_abbrevs));
   31.17 +
   31.18  
   31.19  (* reverted abbrevs *)
   31.20  
    32.1 --- a/src/Pure/facts.ML	Fri Mar 14 12:09:51 2014 +0100
    32.2 +++ b/src/Pure/facts.ML	Fri Mar 14 17:32:11 2014 +0100
    32.3 @@ -26,7 +26,9 @@
    32.4    val check: Context.generic -> T -> xstring * Position.T -> string
    32.5    val intern: T -> xstring -> string
    32.6    val extern: Proof.context -> T -> string -> xstring
    32.7 +  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
    32.8    val lookup: Context.generic -> T -> string -> (bool * thm list) option
    32.9 +  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
   32.10    val defined: T -> string -> bool
   32.11    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   32.12    val dest_static: T list -> T -> (string * thm list) list
   32.13 @@ -155,6 +157,7 @@
   32.14  
   32.15  val intern = Name_Space.intern o space_of;
   32.16  fun extern ctxt = Name_Space.extern ctxt o space_of;
   32.17 +fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
   32.18  
   32.19  val defined = is_some oo (Name_Space.lookup_key o facts_of);
   32.20  
   32.21 @@ -164,6 +167,18 @@
   32.22    | SOME (_, Static ths) => SOME (true, ths)
   32.23    | SOME (_, Dynamic f) => SOME (false, f context));
   32.24  
   32.25 +fun retrieve context facts (xname, pos) =
   32.26 +  let
   32.27 +    val name = check context facts (xname, pos);
   32.28 +    val thms =
   32.29 +      (case lookup context facts name of
   32.30 +        SOME (static, thms) =>
   32.31 +          (if static then ()
   32.32 +           else Context_Position.report_generic context pos (Markup.dynamic_fact name);
   32.33 +           thms)
   32.34 +      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   32.35 +  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
   32.36 +
   32.37  fun fold_static f =
   32.38    Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
   32.39  
   32.40 @@ -195,7 +210,10 @@
   32.41  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   32.42    let
   32.43      val facts' = Name_Space.merge_tables (facts1, facts2);
   32.44 -    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   32.45 +    val props' =
   32.46 +      if Net.is_empty props2 then props1
   32.47 +      else if Net.is_empty props1 then props2
   32.48 +      else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
   32.49    in make_facts facts' props' end;
   32.50  
   32.51  
    33.1 --- a/src/Pure/global_theory.ML	Fri Mar 14 12:09:51 2014 +0100
    33.2 +++ b/src/Pure/global_theory.ML	Fri Mar 14 17:32:11 2014 +0100
    33.3 @@ -11,7 +11,6 @@
    33.4    val intern_fact: theory -> xstring -> string
    33.5    val defined_fact: theory -> string -> bool
    33.6    val hide_fact: bool -> string -> theory -> theory
    33.7 -  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    33.8    val get_thms: theory -> xstring -> thm list
    33.9    val get_thm: theory -> xstring -> thm
   33.10    val all_thms_of: theory -> (string * thm) list
   33.11 @@ -64,31 +63,13 @@
   33.12  fun hide_fact fully name = Data.map (Facts.hide fully name);
   33.13  
   33.14  
   33.15 -(** retrieve theorems **)
   33.16 -
   33.17 -fun get_fact context thy xthmref =
   33.18 -  let
   33.19 -    val facts = facts_of thy;
   33.20 -    val xname = Facts.name_of_ref xthmref;
   33.21 -    val pos = Facts.pos_of_ref xthmref;
   33.22 +(* retrieve theorems *)
   33.23  
   33.24 -    val name =
   33.25 -      (case intern_fact thy xname of
   33.26 -        "_" => "Pure.asm_rl"
   33.27 -      | name => name);
   33.28 -    val res = Facts.lookup context facts name;
   33.29 -  in
   33.30 -    (case res of
   33.31 -      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
   33.32 -    | SOME (static, ths) =>
   33.33 -        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
   33.34 -         if static then ()
   33.35 -         else Context_Position.report_generic context pos (Markup.dynamic_fact name);
   33.36 -         Facts.select xthmref (map (Thm.transfer thy) ths)))
   33.37 -  end;
   33.38 +fun get_thms thy xname =
   33.39 +  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
   33.40  
   33.41 -fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
   33.42 -fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
   33.43 +fun get_thm thy xname =
   33.44 +  Facts.the_single (xname, Position.none) (get_thms thy xname);
   33.45  
   33.46  fun all_thms_of thy =
   33.47    Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
    34.1 --- a/src/Pure/net.ML	Fri Mar 14 12:09:51 2014 +0100
    34.2 +++ b/src/Pure/net.ML	Fri Mar 14 17:32:11 2014 +0100
    34.3 @@ -253,7 +253,7 @@
    34.4        maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
    34.5  
    34.6  fun merge eq (net1, net2) =
    34.7 -  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
    34.8 +  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-canonical merge order!?! *)
    34.9  
   34.10  fun content net = map #2 (dest net);
   34.11  
    35.1 --- a/src/Pure/type.ML	Fri Mar 14 12:09:51 2014 +0100
    35.2 +++ b/src/Pure/type.ML	Fri Mar 14 17:32:11 2014 +0100
    35.3 @@ -26,6 +26,7 @@
    35.4      types: decl Name_Space.table,
    35.5      log_types: string list}
    35.6    val change_base: bool -> tsig -> tsig
    35.7 +  val change_ignore: tsig -> tsig
    35.8    val empty_tsig: tsig
    35.9    val class_space: tsig -> Name_Space.T
   35.10    val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   35.11 @@ -180,6 +181,9 @@
   35.12  fun change_base begin (TSig {classes, default, types, log_types}) =
   35.13    make_tsig (classes, default, Name_Space.change_base begin types, log_types);
   35.14  
   35.15 +fun change_ignore (TSig {classes, default, types, log_types}) =
   35.16 +  make_tsig (classes, default, Name_Space.change_ignore types, log_types);
   35.17 +
   35.18  fun build_tsig (classes, default, types) =
   35.19    let
   35.20      val log_types =
    36.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Fri Mar 14 12:09:51 2014 +0100
    36.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Fri Mar 14 17:32:11 2014 +0100
    36.3 @@ -177,7 +177,7 @@
    36.4  
    36.5  local
    36.6  val (fromsym, fromabbr, tosym, toabbr) =
    36.7 -  read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
    36.8 +  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
    36.9  in
   36.10  val symbol_to_unicode = Symtab.lookup fromsym;
   36.11  val abbrev_to_unicode = Symtab.lookup fromabbr;
    37.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 12:09:51 2014 +0100
    37.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 17:32:11 2014 +0100
    37.3 @@ -53,7 +53,6 @@
    37.4      import JEditToken._
    37.5      Map[String, Byte](
    37.6        Keyword.THY_END -> KEYWORD2,
    37.7 -      Keyword.THY_SCRIPT -> LABEL,
    37.8        Keyword.QED_SCRIPT -> DIGIT,
    37.9        Keyword.PRF_SCRIPT -> DIGIT,
   37.10        Keyword.PRF_ASM -> KEYWORD3,
   37.11 @@ -471,7 +470,8 @@
   37.12            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   37.13            if Path.is_valid(name) =>
   37.14              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
   37.15 -            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
   37.16 +            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
   37.17 +            Some(add(prev, r, (true, XML.Text(text))))
   37.18            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   37.19              Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   37.20            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    38.1 --- a/src/Tools/misc_legacy.ML	Fri Mar 14 12:09:51 2014 +0100
    38.2 +++ b/src/Tools/misc_legacy.ML	Fri Mar 14 17:32:11 2014 +0100
    38.3 @@ -246,10 +246,11 @@
    38.4  val char_vec = Vector.tabulate (62, gensym_char);
    38.5  fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
    38.6  
    38.7 -val gensym_seed = Unsynchronized.ref (0: int);
    38.8 +val gensym_seed = Synchronized.var "gensym_seed" (0: int);
    38.9  
   38.10  in
   38.11 -  fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
   38.12 +  fun gensym pre =
   38.13 +    Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
   38.14  end;
   38.15  
   38.16  
    39.1 --- a/src/ZF/Inductive_ZF.thy	Fri Mar 14 12:09:51 2014 +0100
    39.2 +++ b/src/ZF/Inductive_ZF.thy	Fri Mar 14 17:32:11 2014 +0100
    39.3 @@ -14,8 +14,7 @@
    39.4  theory Inductive_ZF
    39.5  imports Fixedpt QPair Nat_ZF
    39.6  keywords
    39.7 -  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
    39.8 -  "inductive_cases" :: thy_script and
    39.9 +  "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
   39.10    "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   39.11    "elimination" "induction" "case_eqns" "recursor_eqns"
   39.12  begin