--- a/NEWS Wed Aug 11 18:11:07 2010 +0200
+++ b/NEWS Wed Aug 11 18:17:53 2010 +0200
@@ -35,6 +35,10 @@
*** HOL ***
+* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
+in Library/State_Monad has been changed to avoid ambiguities.
+INCOMPATIBILITY.
+
* code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
--- a/src/HOL/Code_Evaluation.thy Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Aug 11 18:17:53 2010 +0200
@@ -64,7 +64,7 @@
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
+ |> Class.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
--- a/src/HOL/Library/State_Monad.thy Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy Wed Aug 11 18:17:53 2010 +0200
@@ -131,7 +131,11 @@
"_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
== "CONST scomp t (\<lambda>p. e)"
"_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
- == "CONST fcomp t e"
+ => "CONST fcomp t e"
+ "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
+ <= "_sdo_final (CONST fcomp t e)"
+ "_sdo_block (_sdo_cons (_sdo_then t) e)"
+ <= "CONST fcomp t (_sdo_block e)"
"_sdo_block (_sdo_cons (_sdo_let p t) bs)"
== "let p = t in _sdo_block bs"
"_sdo_block (_sdo_cons b (_sdo_cons c cs))"
--- a/src/HOL/Statespace/state_space.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Aug 11 18:17:53 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/Datatype/datatype_codegen.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 11 18:17:53 2010 +0200
@@ -115,7 +115,7 @@
#> snd
in
thy
- |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+ |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
|> fold_map add_def dtcos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
--- a/src/HOL/Tools/Function/size.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML Wed Aug 11 18:17:53 2010 +0200
@@ -145,7 +145,7 @@
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
(map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
- ||> Theory_Target.instantiation
+ ||> Class.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
(def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
--- a/src/HOL/Tools/inductive.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Aug 11 18:17:53 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 18:11:07 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Aug 11 18:17:53 2010 +0200
@@ -292,14 +292,14 @@
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;
fun add_primrec_overloaded ops fixes specs thy =
let
- val lthy = Theory_Target.overloading ops thy;
+ val lthy = Overloading.overloading ops 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/quickcheck_generators.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Aug 11 18:17:53 2010 +0200
@@ -86,7 +86,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort random})
+ |> Class.instantiation ([tyco], vs, @{sort random})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
@@ -304,7 +304,7 @@
(HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
in
thy
- |> Theory_Target.instantiation (tycos, vs, @{sort random})
+ |> Class.instantiation (tycos, vs, @{sort random})
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
--- a/src/HOL/Tools/typecopy.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Wed Aug 11 18:17:53 2010 +0200
@@ -116,7 +116,7 @@
thy
|> Code.add_datatype [constr]
|> Code.add_eqn proj_constr
- |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
+ |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
--- a/src/HOL/Tools/typedef.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Wed Aug 11 18:17:53 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/HOL/Typerep.thy Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Typerep.thy Wed Aug 11 18:17:53 2010 +0200
@@ -56,7 +56,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
+ |> Class.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
--- a/src/HOLCF/Tools/pcpodef.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Wed Aug 11 18:17:53 2010 +0200
@@ -203,7 +203,7 @@
val below_eqn = Logic.mk_equals (below_const newT,
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
val lthy3 = thy2
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
val ((_, (_, below_ldef)), lthy4) = lthy3
|> Specification.definition (NONE,
((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
--- a/src/HOLCF/Tools/repdef.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Wed Aug 11 18:17:53 2010 +0200
@@ -112,7 +112,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
--- a/src/Pure/IsaMakefile Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 11 18:17:53 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 18:11:07 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Aug 11 18:17:53 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/class_target.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Wed Aug 11 18:17:53 2010 +0200
@@ -47,6 +47,8 @@
val read_multi_arity: theory -> xstring list * xstring list * xstring
-> string list * (string * sort) list * sort
val type_name: string -> string
+ val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
+ val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
(*subclasses*)
val register_subclass: class * class -> morphism option -> Element.witness option
@@ -580,6 +582,35 @@
(Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
end;
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case instantiation_param lthy b
+ of SOME c => if mx <> NoSyn then syntax_error c
+ else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
+ ##>> AxClass.define_overloaded b_def (c, rhs))
+ ||> confirm_declaration b
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun instantiation arities thy =
+ thy
+ |> init_instantiation arities
+ |> Local_Theory.init NONE ""
+ {define = Generic_Target.define instantiation_foundation,
+ notes = Generic_Target.notes
+ (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ abbrev = Generic_Target.abbrev
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ declaration = K Generic_Target.theory_declaration,
+ syntax_declaration = K Generic_Target.theory_declaration,
+ pretty = single o pretty_instantiation,
+ reinit = instantiation arities o ProofContext.theory_of,
+ exit = Local_Theory.target_of o conclude_instantiation};
+
+fun instantiation_cmd arities thy =
+ instantiation (read_multi_arity thy arities) thy;
+
(* simplified instantiation interface with no class parameter *)
--- a/src/Pure/Isar/expression.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/expression.ML Wed Aug 11 18:17:53 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/generic_target.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Aug 11 18:17:53 2010 +0200
@@ -21,11 +21,21 @@
-> term list -> local_theory -> local_theory)
-> string * bool -> (binding * mixfix) * term -> local_theory
-> (term * term) * local_theory
+
+ val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
+ -> term list * term list -> local_theory -> (term * thm) * local_theory
+ val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
+ -> local_theory -> local_theory
+ val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
+ -> local_theory -> local_theory
end;
structure Generic_Target: GENERIC_TARGET =
struct
+(** lifting primitive to target operations **)
+
(* mixfix syntax *)
fun check_mixfix ctxt (b, extra_tfrees) mx =
@@ -176,4 +186,40 @@
|> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
+
+(** primitive theory operations **)
+
+fun theory_declaration decl lthy =
+ let
+ val global_decl = Morphism.form
+ (Morphism.transform (Local_Theory.global_morphism lthy) decl);
+ in
+ lthy
+ |> Local_Theory.theory (Context.theory_map global_decl)
+ |> Local_Theory.target (Context.proof_map global_decl)
+ end;
+
+fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ let
+ val (const, lthy2) = lthy |> Local_Theory.theory_result
+ (Sign.declare_const ((b, U), mx));
+ val lhs = list_comb (const, type_params @ term_params);
+ val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
+ (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
+ in ((lhs, def), lthy3) end;
+
+fun theory_notes kind global_facts lthy =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
+ in
+ lthy
+ |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
+ end;
+
+fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
+ (Sign.add_abbrev (#1 prmode) (b, t) #->
+ (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+
end;
--- a/src/Pure/Isar/isar_syn.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Aug 11 18:17:53 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 *)
@@ -472,7 +472,7 @@
Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
(Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.print o
- Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
+ Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
@@ -492,7 +492,7 @@
Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
>> Parse.triple1) --| Parse.begin
>> (fn operations => Toplevel.print o
- Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
+ Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
(* code generation *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/named_target.ML Wed Aug 11 18:17:53 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/overloading.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Aug 11 18:17:53 2010 +0200
@@ -19,6 +19,9 @@
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
-> Proof.context -> Proof.context
val set_primary_constraints: Proof.context -> Proof.context
+
+ val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
+ val overloading_cmd: (string * string * bool) list -> theory -> local_theory
end;
structure Overloading: OVERLOADING =
@@ -194,4 +197,40 @@
(Pretty.str "overloading" :: map pr_operation overloading)
end;
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case operation lthy b
+ of SOME (c, checked) => if mx <> NoSyn then syntax_error c
+ else lthy |> Local_Theory.theory_result (declare (c, U)
+ ##>> define checked b_def (c, rhs))
+ ||> confirm b
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun gen_overloading prep_const raw_ops thy =
+ let
+ val ctxt = ProofContext.init_global thy;
+ val ops = raw_ops |> map (fn (name, const, checked) =>
+ (name, Term.dest_Const (prep_const ctxt const), checked));
+ in
+ thy
+ |> init ops
+ |> Local_Theory.init NONE ""
+ {define = Generic_Target.define overloading_foundation,
+ notes = Generic_Target.notes
+ (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ abbrev = Generic_Target.abbrev
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+ Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ declaration = K Generic_Target.theory_declaration,
+ syntax_declaration = K Generic_Target.theory_declaration,
+ pretty = single o pretty,
+ reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
+ exit = Local_Theory.target_of o conclude}
+ end;
+
+val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
+val overloading_cmd = gen_overloading Syntax.read_term;
+
end;
--- a/src/Pure/Isar/specification.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/specification.ML Wed Aug 11 18:17:53 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 18:11:07 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,360 +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,
- instantiation: string list * (string * sort) list * sort,
- overloading: (string * (string * typ) * bool) list}
- val init: string option -> theory -> local_theory
- val context_cmd: xstring -> theory -> local_theory
- val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
- val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
- val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
- val overloading_cmd: (string * string * bool) list -> theory -> local_theory
-end;
-
-structure Theory_Target: THEORY_TARGET =
-struct
-
-(* context data *)
-
-datatype target = Target of {target: string, is_locale: bool,
- is_class: bool, instantiation: string list * (string * sort) list * sort,
- overloading: (string * (string * typ) * bool) list};
-
-fun make_target target is_locale is_class instantiation overloading =
- Target {target = target, is_locale = is_locale,
- is_class = is_class, instantiation = instantiation, overloading = overloading};
-
-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 theory_declaration decl lthy =
- let
- val global_decl = Morphism.form
- (Morphism.transform (Local_Theory.global_morphism lthy) decl);
- in
- lthy
- |> Local_Theory.theory (Context.theory_map global_decl)
- |> Local_Theory.target (Context.proof_map global_decl)
- end;
-
-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 ? theory_declaration decl
- |> Local_Theory.target (add locale locale_decl)
- end;
-
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
- if target = "" then 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 syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- let
- val (const, lthy2) = lthy |> Local_Theory.theory_result
- (Sign.declare_const ((b, U), mx));
- val lhs = list_comb (const, type_params @ term_params);
- val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
- (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
- in ((lhs, def), lthy3) end;
-
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
- 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) =
- 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 instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case Class_Target.instantiation_param lthy b
- of SOME c => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
- ##>> AxClass.define_overloaded b_def (c, rhs))
- ||> Class_Target.confirm_declaration b
- | NONE => lthy |>
- theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case Overloading.operation lthy b
- of SOME (c, checked) => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
- ##>> Overloading.define checked b_def (c, rhs))
- ||> Overloading.confirm b
- | NONE => lthy |>
- theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
- if not is_locale then (NoSyn, NoSyn, mx)
- else if not is_class then (NoSyn, mx, NoSyn)
- else (mx, NoSyn, NoSyn);
-
-fun foundation (ta as Target {target, is_locale, is_class, ...})
- (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- let
- val (mx1, mx2, mx3) = fork_mixfix ta mx;
- val (const, lthy2) = lthy |>
- (case Class_Target.instantiation_param lthy b of
- SOME c =>
- if mx3 <> NoSyn then syntax_error c
- else Local_Theory.theory_result (AxClass.declare_overloaded (c, U))
- ##> Class_Target.confirm_declaration b
- | NONE =>
- (case Overloading.operation lthy b of
- SOME (c, _) =>
- if mx3 <> NoSyn then syntax_error c
- else Local_Theory.theory_result (Overloading.declare (c, U))
- ##> Overloading.confirm b
- | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
- val Const (head, _) = const;
- val lhs = list_comb (const, type_params @ term_params);
- in
- lthy2
- |> pair lhs
- ||>> Local_Theory.theory_result
- (case Overloading.operation lthy b of
- SOME (_, checked) => Overloading.define checked b_def (head, rhs)
- | NONE =>
- if is_some (Class_Target.instantiation_param lthy b)
- then AxClass.define_overloaded b_def (head, rhs)
- else Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)) #>> snd)
- ||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs)
- ||> is_class ? class_target ta
- (Class_Target.declare target ((b, mx1), (type_params, lhs)))
- end;
-
-
-(* notes *)
-
-fun theory_notes kind global_facts lthy =
- let
- val thy = ProofContext.theory_of lthy;
- val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
- in
- lthy
- |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
- end;
-
-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 _ => theory_notes kind global_facts;
-
-
-(* abbrev *)
-
-fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
- (Sign.add_abbrev (#1 prmode) (b, t) #->
- (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
-
-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
- |> 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, instantiation, overloading, ...}) ctxt =
- Pretty.block [Pretty.command "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
- (if not (null overloading) then [Overloading.pretty ctxt]
- else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
- else pretty_thy ctxt target is_class);
-
-
-(* init various targets *)
-
-local
-
-fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) =
- if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
- else if not (null overloading) then Overloading.init overloading
- else 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, instantiation, overloading, ...}) thy =
- thy
- |> init_data ta
- |> Data.put ta
- |> Local_Theory.init NONE (Long_Name.base_name target)
- {define = Generic_Target.define (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 o
- (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
- else if not (null overloading) then Overloading.conclude
- else I)};
-
-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);
-
-fun gen_overloading prep_const raw_ops thy =
- let
- val ctxt = ProofContext.init_global thy;
- val ops = raw_ops |> map (fn (name, const, checked) =>
- (name, Term.dest_Const (prep_const ctxt const), checked));
- in
- thy
- |> Overloading.init ops
- |> Local_Theory.init NONE ""
- {define = Generic_Target.define overloading_foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
- theory_abbrev prmode ((b, mx), t)),
- declaration = fn pervasive => theory_declaration,
- syntax_declaration = fn pervasive => theory_declaration,
- pretty = single o Overloading.pretty,
- reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
- exit = Local_Theory.target_of o Overloading.conclude}
- end;
-
-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;
-
-fun instantiation arities thy =
- thy
- |> Class_Target.init_instantiation arities
- |> Local_Theory.init NONE ""
- {define = Generic_Target.define instantiation_foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
- declaration = fn pervasive => theory_declaration,
- syntax_declaration = fn pervasive => theory_declaration,
- pretty = single o Class_Target.pretty_instantiation,
- reinit = instantiation arities o ProofContext.theory_of,
- exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
-
-fun instantiation_cmd arities thy =
- instantiation (Class_Target.read_multi_arity thy arities) thy;
-
-val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
-val overloading_cmd = gen_overloading Syntax.read_term;
-
-end;
-
-end;
--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 18:17:53 2010 +0200
@@ -102,7 +102,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
@@ -191,7 +191,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 18:11:07 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Aug 11 18:17:53 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 18:11:07 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 11 18:17:53 2010 +0200
@@ -205,12 +205,12 @@
(*local theories and targets*)
use "Isar/local_theory.ML";
+use "Isar/locale.ML";
use "Isar/generic_target.ML";
use "Isar/overloading.ML";
-use "Isar/locale.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 18:11:07 2010 +0200
+++ b/src/Tools/quickcheck.ML Wed Aug 11 18:17:53 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