# HG changeset patch # User ballarin # Date 1516127285 -3600 # Node ID b0ae74b86ef3890c4d913d1e6ab1c938370905d9 # Parent 1caeb087d957f6147c98a5d40d197ac57cf64ea2 Experimental support for rewrite morphisms in locale instances. diff -r 1caeb087d957 -r b0ae74b86ef3 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 15:53:42 2018 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 19:28:05 2018 +0100 @@ -521,6 +521,15 @@ x.lor_triv +subsection \Rewrite morphisms in expressions\ + +interpretation y: logic_o "(\)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\), Not, x, y) \ x \ y" +proof - + show bool_logic_o: "PROP logic_o((\), Not)" by unfold_locales fast+ + show "logic_o.lor_o((\), Not, x, y) \ x \ y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast +qed + + subsection \Inheritance of rewrite morphisms\ locale reflexive = diff -r 1caeb087d957 -r b0ae74b86ef3 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Jan 16 15:53:42 2018 +0100 +++ b/src/HOL/Statespace/state_space.ML Tue Jan 16 19:28:05 2018 +0100 @@ -324,7 +324,7 @@ val components' = map (fn (n,T) => (n,(T,full_name))) components; fun parent_expr (prefix, (_, n, rs)) = - (suffix namespaceN n, (prefix, Expression.Positional rs)); + (suffix namespaceN n, (prefix, (Expression.Positional rs,[]))); val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; @@ -340,9 +340,9 @@ fun projectT T = valueT --> T; fun injectT T = T --> valueT; val locinsts = map (fn T => (project_injectL, - ((encode_type T,false),Expression.Positional + ((encode_type T,false),(Expression.Positional [SOME (Free (project_name T,projectT T)), - SOME (Free ((inject_name T,injectT T)))]))) Ts; + SOME (Free ((inject_name T,injectT T)))],[])))) Ts; val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn), (Binding.name (inject_name T),NONE,NoSyn)]) Ts; val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts; @@ -356,7 +356,7 @@ val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types; val expr = ([(suffix valuetypesN name, - (prefix, Expression.Positional (map SOME pars)))],[]); + (prefix, (Expression.Positional (map SOME pars),[])))],[]); in prove_interpretation_in (fn ctxt => ALLGOALS (solve_tac ctxt (Assumption.all_prems_of ctxt))) (suffix valuetypesN name, expr) thy @@ -364,7 +364,7 @@ fun interprete_parent (prefix, (_, pname, rs)) = let - val expr = ([(pname, (prefix, Expression.Positional rs))],[]) + val expr = ([(pname, (prefix, (Expression.Positional rs,[])))],[]) in prove_interpretation_in (fn ctxt => Locale.intro_locales_tac false ctxt []) (full_name, expr) end; @@ -408,8 +408,8 @@ |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents |> add_locale_cmd name - ([(suffix namespaceN full_name ,(("",false),Expression.Named [])), - (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate + ([(suffix namespaceN full_name ,(("",false),(Expression.Named [],[]))), + (suffix valuetypesN full_name,(("",false),(Expression.Named [],[])))],[]) fixestate |> Proof_Context.theory_of |> fold interprete_parent parents |> add_declaration full_name (declare_declinfo components') diff -r 1caeb087d957 -r b0ae74b86ef3 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Tue Jan 16 15:53:42 2018 +0100 +++ b/src/Pure/Isar/class_declaration.ML Tue Jan 16 19:28:05 2018 +0100 @@ -38,9 +38,9 @@ (Symtab.empty, Symtab.make param_map_inst); val typ_morph = Element.inst_morphism thy (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty); - val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt + val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt |> Expression.cert_goal_expression ([(class, (("", false), - Expression.Named param_map_const))], []); + (Expression.Named param_map_const, [])))], []); val (props, inst_morph) = if null param_map then (raw_props |> map (Morphism.term typ_morph), @@ -156,7 +156,7 @@ (* preprocessing elements, retrieving base sort from type-checked elements *) val raw_supexpr = - (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); + (map (fn sup => (sup, (("", false), (Expression.Positional [], [])))) sups, []); val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups @@ -192,7 +192,7 @@ val supparam_names = map fst supparams; fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); val supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups, + (Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup)), [])))) sups, map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); in (base_sort, supparam_names, supexpr, inferred_elems) end; @@ -354,8 +354,8 @@ | NONE => error "Not in a class target"); val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup); - val expr = ([(sup, (("", false), Expression.Positional []))], []); - val (([props], deps, export), goal_ctxt) = + val expr = ([(sup, (("", false), (Expression.Positional [], [])))], []); + val (([props], _, deps, _, export), goal_ctxt) = Expression.cert_goal_expression expr lthy; val some_prop = try the_single props; val some_dep_morph = try the_single (map snd deps); diff -r 1caeb087d957 -r b0ae74b86ef3 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Jan 16 15:53:42 2018 +0100 +++ b/src/Pure/Isar/expression.ML Tue Jan 16 19:28:05 2018 +0100 @@ -8,7 +8,7 @@ sig (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list - type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list + type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list type expression_i = (string, term) expr * (binding * typ option * mixfix) list type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list @@ -38,9 +38,9 @@ (* Processing of locale expressions *) val cert_goal_expression: expression_i -> Proof.context -> - (term list list * (string * morphism) list * morphism) * Proof.context + (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> - (term list list * (string * morphism) list * morphism) * Proof.context + (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context (* Diagnostic *) val print_dependencies: Proof.context -> bool -> expression -> unit @@ -58,7 +58,7 @@ Positional of 'term option list | Named of (string * 'term) list; -type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list; +type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list; type expression_i = (string, term) expr * (binding * typ option * mixfix) list; type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list; @@ -92,7 +92,7 @@ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); - fun params_inst (loc, (prfx, Positional insts)) = + fun params_inst (loc, (prfx, (Positional insts, eqns))) = let val ps = params_loc loc; val d = length ps - length insts; @@ -103,8 +103,8 @@ else insts @ replicate d NONE; val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); - in (ps', (loc, (prfx, Positional insts'))) end - | params_inst (loc, (prfx, Named insts)) = + in (ps', (loc, (prfx, (Positional insts', eqns)))) end + | params_inst (loc, (prfx, (Named insts, eqns))) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " @@ -112,7 +112,7 @@ val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps else error (quote p ^ " not a parameter of instantiated expression")); - in (ps', (loc, (prfx, Named insts))) end; + in (ps', (loc, (prfx, (Named insts, eqns)))) end; fun params_expr is = let val (is', ps') = fold_map (fn i => fn ps => @@ -232,6 +232,9 @@ fun extract_inst (_, (_, ts)) = map mk_term ts; fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)); +fun extract_eqns es = map (mk_term o snd) es; +fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs; + fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms @@ -266,17 +269,19 @@ in -fun check_autofix insts elems concl ctxt = +fun check_autofix insts eqnss elems concl ctxt = let val inst_cs = map extract_inst insts; + val eqns_cs = map extract_eqns eqnss; val elem_css = map extract_elem elems; val concl_cs = (map o map) mk_propp (map snd concl); (* Type inference *) - val (inst_cs' :: css', ctxt') = - (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt; + val (inst_cs' :: eqns_cs' :: css', ctxt') = + (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in ((map restore_inst (insts ~~ inst_cs'), + map restore_eqns (eqnss ~~ eqns_cs'), map restore_elem (elems ~~ elem_css'), map fst concl ~~ concl_cs'), ctxt') end; @@ -353,27 +358,32 @@ local fun prep_full_context_statement - parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_var_inst prep_expr + parse_typ parse_prop prep_obtains prep_var_elem prep_inst parse_eqn prep_var_inst prep_expr {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 = let val thy = Proof_Context.theory_of ctxt1; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); - fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) = + fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list; val inst' = prep_inst ctxt parm_names inst; + val eqns' = map (apsnd (parse_eqn ctxt)) eqns; val parm_types' = parm_types |> map (Type_Infer.paramify_vars o Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; - val ((insts'', _, _), _) = check_autofix insts' [] [] ctxt; + val eqnss' = eqnss @ [eqns']; + val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; - val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt; - val ctxt'' = Locale.activate_declarations (loc, morph) ctxt; - in (i + 1, insts', ctxt'') end; + val eqns'' = eqnss'' |> List.last; + val (inst_morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt; + val rewrite_morph = eqns'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |> + Element.eq_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity; + val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; + in (i + 1, insts', eqnss', ctxt'') end; fun prep_elem raw_elem ctxt = let @@ -386,10 +396,10 @@ val fors = fold_map prep_var_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd; - val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2); + val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2); fun prep_stmt elems ctxt = - check_autofix insts' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; + check_autofix insts' eqnss' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; val _ = if fixed_frees then () @@ -399,7 +409,7 @@ | frees => error ("Illegal free variables in expression: " ^ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); - val ((insts, elems', concl), ctxt4) = ctxt3 + val ((insts, eqnss, elems', concl), ctxt4) = ctxt3 |> init_body |> fold_map prep_elem raw_elems |-> prep_stmt; @@ -416,21 +426,21 @@ val deps = map (finish_inst ctxt5) insts; val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'; - in ((fixed, deps, elems'', concl), (parms, ctxt5)) end; + in ((fixed, deps, eqnss, elems'', concl), (parms, ctxt5)) end; in fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) Obtain.cert_obtains - Proof_Context.cert_var make_inst Proof_Context.cert_var (K I) x; + Proof_Context.cert_var make_inst (K I) Proof_Context.cert_var (K I) x; fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains - Proof_Context.read_var make_inst Proof_Context.cert_var (K I) x; + Proof_Context.read_var make_inst (K I) Proof_Context.cert_var (K I) x; fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains - Proof_Context.read_var parse_inst Proof_Context.read_var check_expr x; + Proof_Context.read_var parse_inst (Syntax.parse_prop) Proof_Context.read_var check_expr x; end; @@ -441,7 +451,7 @@ fun prep_statement prep activate raw_elems raw_stmt ctxt = let - val ((_, _, elems, concl), _) = + val ((_, _, _, elems, concl), _) = prep {strict = true, do_close = false, fixed_frees = true} ([], []) I raw_elems raw_stmt ctxt; val ctxt' = ctxt @@ -467,9 +477,10 @@ fun prep_declaration prep activate raw_import init_body raw_elems ctxt = let - val ((fixed, deps, elems, _), (parms, ctxt0)) = + val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) = prep {strict = false, do_close = true, fixed_frees = false} raw_import init_body raw_elems (Element.Shows []) ctxt; + val _ = null (flat eqnss) orelse error "Illegal replaces clause(s) in declaration of locale"; (* Declare parameters and imported facts *) val ctxt' = ctxt |> fix_params fixed @@ -505,11 +516,12 @@ let val thy = Proof_Context.theory_of ctxt; - val ((fixed, deps, _, _), _) = + val ((fixed, deps, eqnss, _, _), _) = prep {strict = true, do_close = true, fixed_frees = true} expression I [] (Element.Shows []) ctxt; (* proof obligations *) val propss = map (props_of thy) deps; + val eq_propss = (map o map) snd eqnss; val goal_ctxt = ctxt |> fix_params fixed @@ -522,7 +534,7 @@ val export' = Morphism.morphism "Expression.prep_goal" {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]}; - in ((propss, deps, export'), goal_ctxt) end; + in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end; in @@ -844,7 +856,7 @@ fun print_dependencies ctxt clean expression = let - val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt; + val ((_, _, deps, _, export), expr_ctxt) = read_goal_expression expression ctxt; val export' = if clean then Morphism.identity else export; in Locale.print_dependencies expr_ctxt clean export' deps diff -r 1caeb087d957 -r b0ae74b86ef3 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Tue Jan 16 15:53:42 2018 +0100 +++ b/src/Pure/Isar/interpretation.ML Tue Jan 16 19:28:05 2018 +0100 @@ -55,7 +55,7 @@ local -fun augment_with_def prep_term deps ((name, atts), ((b, mx), raw_rhs)) lthy = +fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy = let val rhs = prep_term lthy raw_rhs; val lthy' = Variable.declare_term rhs lthy; @@ -63,7 +63,7 @@ Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy'; in (def, lthy'') end; -fun augment_with_defs prep_term [] deps ctxt = ([], ctxt) +fun augment_with_defs _ [] _ ctxt = ([], ctxt) (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) | augment_with_defs prep_term raw_defs deps lthy = let @@ -71,7 +71,7 @@ Local_Theory.open_target lthy ||> fold Locale.activate_declarations deps; val (inner_defs, inner_lthy') = - fold_map (augment_with_def prep_term deps) raw_defs inner_lthy; + fold_map (augment_with_def prep_term) raw_defs inner_lthy; val lthy' = inner_lthy' |> Local_Theory.close_target; @@ -79,9 +79,11 @@ map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs in (def_eqns, lthy') end; -fun prep_eqns prep_props prep_attr [] deps ctxt = ([], []) +fun prep_eqns _ _ [] _ _ = ([], []) | prep_eqns prep_props prep_attr raw_eqns deps ctxt = let + (* FIXME incompatibility, creating context for parsing rewrites equation may fail in + presence of replaces clause *) val ctxt' = fold Locale.activate_declarations deps ctxt; val eqns = (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns; @@ -91,13 +93,13 @@ fun prep_interpretation prep_expr prep_term prep_props prep_attr expression raw_defs raw_eqns initial_ctxt = let - val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; + val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; val (def_eqns, def_ctxt) = augment_with_defs prep_term raw_defs deps expr_ctxt; val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt; val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; + in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; in @@ -119,13 +121,17 @@ fun meta_rewrite eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); -fun note_eqns_register pos note activate deps witss def_eqns eqns attrss export export' ctxt = +fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt = let + val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms); + val factss = + map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss; + val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; val facts = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) - attrss eqns; - val (eqns', ctxt') = ctxt + attrss thms'; + val (eqns', ctxt'') = ctxt' |> note Thm.theoremK facts |-> meta_rewrite; val dep_morphs = @@ -134,23 +140,23 @@ $> Element.satisfy_morphism (map (Element.transform_witness export') wits) $> Morphism.binding_morphism "position" (Binding.set_pos pos) in (dep, morph') end) deps witss; - fun activate' dep_morph ctxt = + fun activate' (dep_morph, eqns) ctxt = activate dep_morph - (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) + (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns'))) export ctxt; - in ctxt' |> fold activate' dep_morphs end; + in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end; in fun generic_interpretation prep_interpretation setup_proof note add_registration expression raw_defs raw_eqns initial_ctxt = let - val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = + val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = prep_interpretation expression raw_defs raw_eqns initial_ctxt; val pos = Position.thread_data (); fun after_qed witss eqns = - note_eqns_register pos note add_registration deps witss def_eqns eqns attrss export export'; - in setup_proof after_qed propss eqns goal_ctxt end; + note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export'; + in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end; end; diff -r 1caeb087d957 -r b0ae74b86ef3 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Tue Jan 16 15:53:42 2018 +0100 +++ b/src/Pure/Isar/parse_spec.ML Tue Jan 16 19:28:05 2018 +0100 @@ -111,9 +111,10 @@ fun plus1_unless test scan = scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); -val instance = Parse.where_ |-- +val instance = Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || - Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; + Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) -- + (Scan.optional (Parse.$$$ "replaces" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []); in @@ -133,7 +134,7 @@ val expr2 = Parse.position Parse.name; val expr1 = locale_prefix -- expr2 -- - Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); + instance >> (fn ((p, l), i) => (l, (p, i))); val expr0 = plus1_unless locale_keyword expr1; in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; diff -r 1caeb087d957 -r b0ae74b86ef3 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Jan 16 15:53:42 2018 +0100 +++ b/src/Pure/Pure.thy Tue Jan 16 19:28:05 2018 +0100 @@ -10,7 +10,7 @@ "\" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command - and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" + and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "replaces" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw