--- a/src/HOL/Statespace/state_space.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Aug 11 14:45:38 2010 +0200
@@ -348,7 +348,7 @@
fun add_declaration name decl thy =
thy
- |> Theory_Target.init name
+ |> Named_Target.init name
|> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
|> Local_Theory.exit_global;
--- a/src/HOL/Tools/inductive.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Aug 11 14:45:38 2010 +0200
@@ -998,7 +998,7 @@
let
val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
val ctxt' = thy
- |> Theory_Target.init NONE
+ |> Named_Target.init NONE
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
|> Local_Theory.exit;
val info = #2 (the_inductive ctxt' name);
--- a/src/HOL/Tools/primrec.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Aug 11 14:45:38 2010 +0200
@@ -292,7 +292,7 @@
fun add_primrec_global fixes specs thy =
let
- val lthy = Theory_Target.init NONE thy;
+ val lthy = Named_Target.init NONE thy;
val ((ts, simps), lthy') = add_primrec fixes specs lthy;
val simps' = ProofContext.export lthy' lthy simps;
in ((ts, simps'), Local_Theory.exit_global lthy') end;
--- a/src/HOL/Tools/typedef.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Wed Aug 11 14:45:38 2010 +0200
@@ -268,7 +268,7 @@
in typedef_result inhabited lthy' end;
fun add_typedef_global def opt_name typ set opt_morphs tac =
- Theory_Target.init NONE
+ Named_Target.init NONE
#> add_typedef def opt_name typ set opt_morphs tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
--- a/src/Pure/IsaMakefile Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 11 14:45:38 2010 +0200
@@ -127,6 +127,7 @@
Isar/local_theory.ML \
Isar/locale.ML \
Isar/method.ML \
+ Isar/named_target.ML \
Isar/object_logic.ML \
Isar/obtain.ML \
Isar/outer_syntax.ML \
@@ -144,7 +145,6 @@
Isar/skip_proof.ML \
Isar/spec_rules.ML \
Isar/specification.ML \
- Isar/theory_target.ML \
Isar/token.ML \
Isar/toplevel.ML \
Isar/typedecl.ML \
--- a/src/Pure/Isar/class.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Aug 11 14:45:38 2010 +0200
@@ -7,7 +7,7 @@
signature CLASS =
sig
include CLASS_TARGET
- (*FIXME the split into class_target.ML, theory_target.ML and
+ (*FIXME the split into class_target.ML, Named_Target.ML and
class.ML is artificial*)
val class: binding -> class list -> Element.context_i list
@@ -296,7 +296,7 @@
Context.theory_map (Locale.add_registration (class, base_morph)
(Option.map (rpair true) eq_morph) export_morph)
#> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
- |> Theory_Target.init (SOME class)
+ |> Named_Target.init (SOME class)
|> pair class
end;
@@ -316,7 +316,7 @@
let
val thy = ProofContext.theory_of lthy;
val proto_sup = prep_class thy raw_sup;
- val proto_sub = case Theory_Target.peek lthy
+ val proto_sub = case Named_Target.peek lthy
of {is_class = false, ...} => error "Not in a class context"
| {target, ...} => target;
val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
@@ -329,7 +329,7 @@
fun after_qed some_wit =
ProofContext.theory (register_subclass (sub, sup)
some_dep_morph some_wit export)
- #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
+ #> ProofContext.theory_of #> Named_Target.init (SOME sub);
in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed some_prop =
--- a/src/Pure/Isar/expression.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/expression.ML Wed Aug 11 14:45:38 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')
- |> Theory_Target.init (SOME name)
+ |> Named_Target.init (SOME 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 = Theory_Target.init (SOME target) thy;
+ val target_ctxt = Named_Target.init (SOME 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/isar_syn.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Aug 11 14:45:38 2010 +0200
@@ -406,7 +406,7 @@
val _ =
Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
(Parse.name --| Parse.begin >> (fn name =>
- Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
+ Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
(* locales *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/named_target.ML Wed Aug 11 14:45:38 2010 +0200
@@ -0,0 +1,211 @@
+(* Title: Pure/Isar/theory_target.ML
+ Author: Makarius
+ Author: Florian Haftmann, TU Muenchen
+
+Targets for theory, locale and class.
+*)
+
+signature NAMED_TARGET =
+sig
+ val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
+ val init: string option -> theory -> local_theory
+ val context_cmd: xstring -> theory -> local_theory
+end;
+
+structure Named_Target: NAMED_TARGET =
+struct
+
+(* context data *)
+
+datatype target = Target of {target: string, is_locale: bool, is_class: bool};
+
+fun make_target target is_locale is_class =
+ Target {target = target, is_locale = is_locale, is_class = is_class};
+
+val global_target = make_target "" false false;
+
+structure Data = Proof_Data
+(
+ type T = target;
+ fun init _ = global_target;
+);
+
+val peek = (fn Target args => args) o Data.get;
+
+
+(* generic declarations *)
+
+fun locale_declaration locale { syntax, pervasive } decl lthy =
+ let
+ val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
+ val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
+ in
+ lthy
+ |> pervasive ? Generic_Target.theory_declaration decl
+ |> Local_Theory.target (add locale locale_decl)
+ end;
+
+fun target_declaration (Target {target, ...}) { syntax, pervasive } =
+ if target = "" then Generic_Target.theory_declaration
+ else locale_declaration target { syntax = syntax, pervasive = pervasive };
+
+
+(* consts in locales *)
+
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
+ let
+ val b' = Morphism.binding phi b;
+ val rhs' = Morphism.term phi rhs;
+ val arg = (b', Term.close_schematic_term rhs');
+ val same_shape = Term.aconv_untyped (rhs, rhs');
+ (* FIXME workaround based on educated guess *)
+ val prefix' = Binding.prefix_of b';
+ val is_canonical_class = is_class andalso
+ (Binding.eq_name (b, b')
+ andalso not (null prefix')
+ andalso List.last prefix' = (Class_Target.class_prefix target, false)
+ orelse same_shape);
+ in
+ not is_canonical_class ?
+ (Context.mapping_result
+ (Sign.add_abbrev Print_Mode.internal arg)
+ (ProofContext.add_abbrev Print_Mode.internal arg)
+ #-> (fn (lhs' as Const (d, _), _) =>
+ same_shape ?
+ (Context.mapping
+ (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
+ Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
+ end;
+
+fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
+ locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
+
+fun class_target (Target {target, ...}) f =
+ Local_Theory.raw_theory f #>
+ Local_Theory.target (Class_Target.refresh_syntax target);
+
+
+(* define *)
+
+fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+ Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+ #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
+ #> pair (lhs, def))
+
+fun class_foundation (ta as Target {target, ...})
+ (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+ Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+ #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
+ #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
+ #> pair (lhs, def))
+
+fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
+ if is_class then class_foundation ta
+ else if is_locale then locale_foundation ta
+ else Generic_Target.theory_foundation;
+
+
+(* notes *)
+
+fun locale_notes locale kind global_facts local_facts lthy =
+ let
+ val global_facts' = Attrib.map_facts (K I) global_facts;
+ val local_facts' = Element.facts_map
+ (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
+ in
+ lthy
+ |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
+ end
+
+fun target_notes (ta as Target {target, is_locale, ...}) =
+ if is_locale then locale_notes target
+ else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+
+
+(* abbrev *)
+
+fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
+ (Sign.add_abbrev Print_Mode.internal (b, t)) #->
+ (fn (lhs, _) => locale_const_declaration ta prmode
+ ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+
+fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
+ prmode (b, mx) (global_rhs, t') xs lthy =
+ if is_locale
+ then lthy
+ |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+ |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
+ else lthy
+ |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+
+
+(* pretty *)
+
+fun pretty_thy ctxt target is_class =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val target_name =
+ [Pretty.command (if is_class then "class" else "locale"),
+ Pretty.str (" " ^ Locale.extern thy target)];
+ val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
+ (#1 (ProofContext.inferred_fixes ctxt));
+ val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
+ (Assumption.all_assms_of ctxt);
+ val elems =
+ (if null fixes then [] else [Element.Fixes fixes]) @
+ (if null assumes then [] else [Element.Assumes assumes]);
+ in
+ if target = "" then []
+ else if null elems then [Pretty.block target_name]
+ else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
+ map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
+ end;
+
+fun pretty (Target {target, is_class, ...}) ctxt =
+ Pretty.block [Pretty.command "theory", Pretty.brk 1,
+ Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
+ pretty_thy ctxt target is_class;
+
+
+(* init various targets *)
+
+local
+
+fun init_data (Target {target, is_locale, is_class}) =
+ if not is_locale then ProofContext.init_global
+ else if not is_class then Locale.init target
+ else Class_Target.init target;
+
+fun init_target (ta as Target {target, ...}) thy =
+ thy
+ |> init_data ta
+ |> Data.put ta
+ |> Local_Theory.init NONE (Long_Name.base_name target)
+ {define = Generic_Target.define (target_foundation ta),
+ notes = Generic_Target.notes (target_notes ta),
+ abbrev = Generic_Target.abbrev (target_abbrev ta),
+ declaration = fn pervasive => target_declaration ta
+ { syntax = false, pervasive = pervasive },
+ syntax_declaration = fn pervasive => target_declaration ta
+ { syntax = true, pervasive = pervasive },
+ pretty = pretty ta,
+ reinit = init_target ta o ProofContext.theory_of,
+ exit = Local_Theory.target_of};
+
+fun named_target _ NONE = global_target
+ | named_target thy (SOME target) =
+ if Locale.defined thy target
+ then make_target target true (Class_Target.is_class thy target)
+ else error ("No such locale: " ^ quote target);
+
+in
+
+fun init target thy = init_target (named_target thy target) thy;
+
+fun context_cmd "-" thy = init NONE thy
+ | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
+
+end;
+
+end;
--- a/src/Pure/Isar/specification.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/specification.ML Wed Aug 11 14:45:38 2010 +0200
@@ -185,7 +185,7 @@
(*facts*)
val (facts, facts_lthy) = axioms_thy
- |> Theory_Target.init NONE
+ |> Named_Target.init NONE
|> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
|> Local_Theory.notes axioms;
--- a/src/Pure/Isar/theory_target.ML Wed Aug 11 14:41:16 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-(* Title: Pure/Isar/theory_target.ML
- Author: Makarius
- Author: Florian Haftmann, TU Muenchen
-
-Common theory/locale/class/instantiation/overloading targets.
-*)
-
-signature THEORY_TARGET =
-sig
- val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
- val init: string option -> theory -> local_theory
- val context_cmd: xstring -> theory -> local_theory
-end;
-
-structure Theory_Target: THEORY_TARGET =
-struct
-
-(* context data *)
-
-datatype target = Target of {target: string, is_locale: bool, is_class: bool};
-
-fun make_target target is_locale is_class =
- Target {target = target, is_locale = is_locale, is_class = is_class};
-
-val global_target = make_target "" false false;
-
-structure Data = Proof_Data
-(
- type T = target;
- fun init _ = global_target;
-);
-
-val peek = (fn Target args => args) o Data.get;
-
-
-(* generic declarations *)
-
-fun locale_declaration locale { syntax, pervasive } decl lthy =
- let
- val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
- val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
- in
- lthy
- |> pervasive ? Generic_Target.theory_declaration decl
- |> Local_Theory.target (add locale locale_decl)
- end;
-
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
- if target = "" then Generic_Target.theory_declaration
- else locale_declaration target { syntax = syntax, pervasive = pervasive };
-
-
-(* consts in locales *)
-
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
- let
- val b' = Morphism.binding phi b;
- val rhs' = Morphism.term phi rhs;
- val arg = (b', Term.close_schematic_term rhs');
- val same_shape = Term.aconv_untyped (rhs, rhs');
- (* FIXME workaround based on educated guess *)
- val prefix' = Binding.prefix_of b';
- val is_canonical_class = is_class andalso
- (Binding.eq_name (b, b')
- andalso not (null prefix')
- andalso List.last prefix' = (Class_Target.class_prefix target, false)
- orelse same_shape);
- in
- not is_canonical_class ?
- (Context.mapping_result
- (Sign.add_abbrev Print_Mode.internal arg)
- (ProofContext.add_abbrev Print_Mode.internal arg)
- #-> (fn (lhs' as Const (d, _), _) =>
- same_shape ?
- (Context.mapping
- (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
- Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
- end;
-
-fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
- locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
-
-fun class_target (Target {target, ...}) f =
- Local_Theory.raw_theory f #>
- Local_Theory.target (Class_Target.refresh_syntax target);
-
-
-(* define *)
-
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
- Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
- #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
- #> pair (lhs, def))
-
-fun class_foundation (ta as Target {target, ...})
- (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
- Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
- #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
- #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
- #> pair (lhs, def))
-
-fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
- if is_class then class_foundation ta
- else if is_locale then locale_foundation ta
- else Generic_Target.theory_foundation;
-
-
-(* notes *)
-
-fun locale_notes locale kind global_facts local_facts lthy =
- let
- val global_facts' = Attrib.map_facts (K I) global_facts;
- val local_facts' = Element.facts_map
- (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
- in
- lthy
- |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
- end
-
-fun target_notes (ta as Target {target, is_locale, ...}) =
- if is_locale then locale_notes target
- else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
-
-
-(* abbrev *)
-
-fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
- (Sign.add_abbrev Print_Mode.internal (b, t)) #->
- (fn (lhs, _) => locale_const_declaration ta prmode
- ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
-
-fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
- prmode (b, mx) (global_rhs, t') xs lthy =
- if is_locale
- then lthy
- |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
- |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
- else lthy
- |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
-
-
-(* pretty *)
-
-fun pretty_thy ctxt target is_class =
- let
- val thy = ProofContext.theory_of ctxt;
- val target_name =
- [Pretty.command (if is_class then "class" else "locale"),
- Pretty.str (" " ^ Locale.extern thy target)];
- val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
- (#1 (ProofContext.inferred_fixes ctxt));
- val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
- (Assumption.all_assms_of ctxt);
- val elems =
- (if null fixes then [] else [Element.Fixes fixes]) @
- (if null assumes then [] else [Element.Assumes assumes]);
- in
- if target = "" then []
- else if null elems then [Pretty.block target_name]
- else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
- map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
- end;
-
-fun pretty (Target {target, is_class, ...}) ctxt =
- Pretty.block [Pretty.command "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
- pretty_thy ctxt target is_class;
-
-
-(* init various targets *)
-
-local
-
-fun init_data (Target {target, is_locale, is_class}) =
- if not is_locale then ProofContext.init_global
- else if not is_class then Locale.init target
- else Class_Target.init target;
-
-fun init_target (ta as Target {target, ...}) thy =
- thy
- |> init_data ta
- |> Data.put ta
- |> Local_Theory.init NONE (Long_Name.base_name target)
- {define = Generic_Target.define (target_foundation ta),
- notes = Generic_Target.notes (target_notes ta),
- abbrev = Generic_Target.abbrev (target_abbrev ta),
- declaration = fn pervasive => target_declaration ta
- { syntax = false, pervasive = pervasive },
- syntax_declaration = fn pervasive => target_declaration ta
- { syntax = true, pervasive = pervasive },
- pretty = pretty ta,
- reinit = init_target ta o ProofContext.theory_of,
- exit = Local_Theory.target_of};
-
-fun named_target _ NONE = global_target
- | named_target thy (SOME target) =
- if Locale.defined thy target
- then make_target target true (Class_Target.is_class thy target)
- else error ("No such locale: " ^ quote target);
-
-in
-
-fun init target thy = init_target (named_target thy target) thy;
-
-fun context_cmd "-" thy = init NONE thy
- | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
-
-end;
-
-end;
--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 14:45:38 2010 +0200
@@ -103,7 +103,7 @@
(* local theory wrappers *)
-val loc_init = Theory_Target.context_cmd;
+val loc_init = Named_Target.context_cmd;
val loc_exit = Local_Theory.exit_global;
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -194,7 +194,7 @@
(* print state *)
-val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
+val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
fun print_state_context state =
(case try node_of state of
--- a/src/Pure/Isar/typedecl.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Aug 11 14:45:38 2010 +0200
@@ -75,7 +75,7 @@
end;
fun typedecl_global decl =
- Theory_Target.init NONE
+ Named_Target.init NONE
#> typedecl decl
#> Local_Theory.exit_result_global Morphism.typ;
@@ -115,7 +115,7 @@
end;
fun abbrev_global decl rhs =
- Theory_Target.init NONE
+ Named_Target.init NONE
#> abbrev decl rhs
#> Local_Theory.exit_result_global (K I);
--- a/src/Pure/ROOT.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 11 14:45:38 2010 +0200
@@ -210,7 +210,7 @@
use "Isar/overloading.ML";
use "axclass.ML";
use "Isar/class_target.ML";
-use "Isar/theory_target.ML";
+use "Isar/named_target.ML";
use "Isar/expression.ML";
use "Isar/class.ML";
--- a/src/Tools/quickcheck.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Tools/quickcheck.ML Wed Aug 11 14:45:38 2010 +0200
@@ -219,7 +219,7 @@
| strip t = t;
val {goal = st, ...} = Proof.raw_goal state;
val (gi, frees) = Logic.goal_params (prop_of st) i;
- val some_locale = case (#target o Theory_Target.peek) lthy
+ val some_locale = case (#target o Named_Target.peek) lthy
of "" => NONE
| locale => SOME locale;
val assms = if no_assms then [] else case some_locale