--- a/src/HOL/Statespace/state_space.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Aug 12 13:28:18 2010 +0200
@@ -466,7 +466,7 @@
(suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate
|> ProofContext.theory_of
|> fold interprete_parent parents
- |> add_declaration (SOME full_name) (declare_declinfo components')
+ |> add_declaration full_name (declare_declinfo components')
end;
--- a/src/Pure/Isar/class_declaration.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Aug 12 13:28:18 2010 +0200
@@ -290,7 +290,7 @@
Context.theory_map (Locale.add_registration (class, base_morph)
(Option.map (rpair true) eq_morph) export_morph)
#> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
- |> Named_Target.init (SOME class)
+ |> Named_Target.init class
|> pair class
end;
@@ -323,7 +323,7 @@
fun after_qed some_wit =
ProofContext.theory (Class.register_subclass (sub, sup)
some_dep_morph some_wit export)
- #> ProofContext.theory_of #> Named_Target.init (SOME sub);
+ #> ProofContext.theory_of #> Named_Target.init sub;
in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed some_prop =
--- a/src/Pure/Isar/expression.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/expression.ML Thu Aug 12 13:28:18 2010 +0200
@@ -775,7 +775,7 @@
val loc_ctxt = thy'
|> Locale.register_locale binding (extraTs, params)
(asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
- |> Named_Target.init (SOME name)
+ |> Named_Target.init name
|> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
in (name, loc_ctxt) end;
@@ -870,7 +870,7 @@
fun gen_sublocale prep_expr intern raw_target expression thy =
let
val target = intern thy raw_target;
- val target_ctxt = Named_Target.init (SOME target) thy;
+ val target_ctxt = Named_Target.init target thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
fun after_qed witss = ProofContext.theory
(fold (fn ((dep, morph), wits) => Locale.add_dependency
--- a/src/Pure/Isar/named_target.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Thu Aug 12 13:28:18 2010 +0200
@@ -8,7 +8,7 @@
signature NAMED_TARGET =
sig
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
- val init: string option -> theory -> local_theory
+ val init: string -> theory -> local_theory
val theory_init: theory -> local_theory
val context_cmd: xstring -> theory -> local_theory
end;
@@ -25,8 +25,8 @@
val global_target = Target {target = "", is_locale = false, is_class = false};
-fun named_target _ NONE = global_target
- | named_target thy (SOME locale) =
+fun named_target _ "" = global_target
+ | named_target thy locale =
if Locale.defined thy locale
then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
else error ("No such locale: " ^ quote locale);
@@ -205,8 +205,8 @@
val theory_init = init_target global_target;
-fun context_cmd "-" thy = init NONE thy
- | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
+fun context_cmd "-" thy = init "" thy
+ | context_cmd target thy = init (Locale.intern thy target) thy;
end;
--- a/src/Pure/Isar/toplevel.ML Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 12 13:28:18 2010 +0200
@@ -112,8 +112,7 @@
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
| loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
| loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
- val target_name = #target (Named_Target.peek lthy);
- val target = if target_name = "" then NONE else SOME target_name;
+ val target = #target (Named_Target.peek lthy);
in Context.Proof (Named_Target.init target (loc_exit lthy')) end;