# HG changeset patch # User wenzelm # Date 1281543473 -7200 # Node ID ea1ee55aa41f49e163e2d51b3dcc83b8152d7614 # Parent 480b2de9927c76c8f45833bbbdb5cda650f37748# Parent f6c1e169f51b36c1aded9594834ba7fb90acab2a merged diff -r f6c1e169f51b -r ea1ee55aa41f NEWS --- 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. diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Code_Evaluation.thy --- 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 diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Library/State_Monad.thy --- 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 (\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))" diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Statespace/state_space.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/Datatype/datatype_codegen.ML --- 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) diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/Function/size.ML --- 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)) diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/inductive.ML --- 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); diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/primrec.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/quickcheck_generators.ML --- 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 => diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/typecopy.ML --- 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))) diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/typedef.ML --- 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); diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Typerep.thy --- 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 diff -r f6c1e169f51b -r ea1ee55aa41f src/HOLCF/Tools/pcpodef.ML --- 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)); diff -r f6c1e169f51b -r ea1ee55aa41f src/HOLCF/Tools/repdef.ML --- 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) = diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/IsaMakefile --- 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 \ diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/class.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 = diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/class_target.ML --- 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 *) diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/expression.ML --- 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 diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/generic_target.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/isar_syn.ML --- 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 *) diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/named_target.ML --- /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; diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/overloading.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/specification.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/theory_target.ML --- 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; diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/toplevel.ML --- 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 diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/typedecl.ML --- 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); diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/ROOT.ML --- 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"; diff -r f6c1e169f51b -r ea1ee55aa41f src/Tools/quickcheck.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