# HG changeset patch # User wenzelm # Date 1237496737 -3600 # Node ID 4216e9c70cfe6766df47dcc54926fd46964bfd8d # Parent eb827cd69fd3916fb87678f4312243d6c6c424e0# Parent c87a3350f5a9f3de76dc925107b700599fda67fc merged diff -r eb827cd69fd3 -r 4216e9c70cfe src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Mar 19 08:13:10 2009 -0700 +++ b/src/HOL/Library/Multiset.thy Thu Mar 19 22:05:37 2009 +0100 @@ -1623,8 +1623,8 @@ msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv, mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac, mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps, - smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1}, - reduction_pair=@{thm ms_reduction_pair} + smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1}, + reduction_pair= @{thm ms_reduction_pair} }) end *} diff -r eb827cd69fd3 -r 4216e9c70cfe src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Mar 19 22:05:37 2009 +0100 @@ -106,8 +106,8 @@ val ak_type = Type (Sign.intern_type thy1 ak,[]) val ak_sign = Sign.intern_const thy1 ak - val inj_type = @{typ nat}-->ak_type - val inj_on_type = inj_type-->(@{typ "nat set"})-->@{typ bool} + val inj_type = @{typ nat} --> ak_type + val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool} (* first statement *) val stmnt1 = HOLogic.mk_Trueprop diff -r eb827cd69fd3 -r 4216e9c70cfe src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Mar 19 22:05:37 2009 +0100 @@ -23,7 +23,7 @@ val false_tm = @{cterm "False"}; val zdvd1_eq = @{thm "zdvd1_eq"}; val presburger_ss = @{simpset} addsimps [zdvd1_eq]; -val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac}); +val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac}); val iT = HOLogic.intT val bT = HOLogic.boolT; diff -r eb827cd69fd3 -r 4216e9c70cfe src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/HOLCF/Tools/domain/domain_library.ML Thu Mar 19 22:05:37 2009 +0100 @@ -125,37 +125,37 @@ infix 0 ==; fun S == T = %%:"==" $ S $ T; infix 1 ===; fun S === T = %%:"op =" $ S $ T; infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); -infix 1 <<; fun S << T = %%:@{const_name Porder.sq_le} $ S $ T; +infix 1 <<; fun S << T = %%: @{const_name Porder.sq_le} $ S $ T; infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); -infix 9 ` ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x; +infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; infix 9 `% ; fun f`% s = f` %: s; infix 9 `%%; fun f`%%s = f` %%:s; -fun mk_adm t = %%:@{const_name adm} $ t; -fun mk_compact t = %%:@{const_name compact} $ t; -val ID = %%:@{const_name ID}; -fun mk_strictify t = %%:@{const_name strictify}`t; -fun mk_cfst t = %%:@{const_name cfst}`t; -fun mk_csnd t = %%:@{const_name csnd}`t; +fun mk_adm t = %%: @{const_name adm} $ t; +fun mk_compact t = %%: @{const_name compact} $ t; +val ID = %%: @{const_name ID}; +fun mk_strictify t = %%: @{const_name strictify}`t; +fun mk_cfst t = %%: @{const_name cfst}`t; +fun mk_csnd t = %%: @{const_name csnd}`t; (*val csplitN = "Cprod.csplit";*) (*val sfstN = "Sprod.sfst";*) (*val ssndN = "Sprod.ssnd";*) -fun mk_ssplit t = %%:@{const_name ssplit}`t; -fun mk_sinl t = %%:@{const_name sinl}`t; -fun mk_sinr t = %%:@{const_name sinr}`t; -fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y; -fun mk_up t = %%:@{const_name up}`t; -fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u; +fun mk_ssplit t = %%: @{const_name ssplit}`t; +fun mk_sinl t = %%: @{const_name sinl}`t; +fun mk_sinr t = %%: @{const_name sinr}`t; +fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; +fun mk_up t = %%: @{const_name up}`t; +fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; val ONE = @{term ONE}; val TT = @{term TT}; val FF = @{term FF}; -fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z; -fun mk_fix t = %%:@{const_name fix}`t; -fun mk_return t = %%:@{const_name Fixrec.return}`t; -val mk_fail = %%:@{const_name Fixrec.fail}; +fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z; +fun mk_fix t = %%: @{const_name fix}`t; +fun mk_return t = %%: @{const_name Fixrec.return}`t; +val mk_fail = %%: @{const_name Fixrec.fail}; -fun mk_branch t = %%:@{const_name Fixrec.branch} $ t; +fun mk_branch t = %%: @{const_name Fixrec.branch} $ t; val pcpoS = @{sort pcpo}; @@ -171,14 +171,14 @@ fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); -fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T); +fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T); fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T; -val UU = %%:@{const_name UU}; +infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T; +val UU = %%: @{const_name UU}; fun strict f = f`UU === UU; fun defined t = t ~= UU; -fun cpair (t,u) = %%:@{const_name cpair}`t`u; -fun spair (t,u) = %%:@{const_name spair}`t`u; +fun cpair (t,u) = %%: @{const_name cpair}`t`u; +fun spair (t,u) = %%: @{const_name spair}`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) | mk_ctuple ts = foldr1 cpair ts; fun mk_stuple [] = ONE @@ -186,7 +186,7 @@ fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; fun mk_maybeT T = Type ("Fixrec.maybe",[T]); -fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2; +fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; val mk_ctuple_pat = foldr1 cpair_pat; fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/General/ROOT.ML Thu Mar 19 22:05:37 2009 +0100 @@ -15,6 +15,7 @@ use "seq.ML"; use "position.ML"; use "symbol_pos.ML"; +use "antiquote.ML"; use "../ML/ml_lex.ML"; use "../ML/ml_parse.ML"; use "secure.ML"; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/General/antiquote.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/antiquote.ML Thu Mar 19 22:05:37 2009 +0100 @@ -0,0 +1,95 @@ +(* Title: Pure/General/antiquote.ML + Author: Markus Wenzel, TU Muenchen + +Text with antiquotations of inner items (types, terms, theorems etc.). +*) + +signature ANTIQUOTE = +sig + datatype 'a antiquote = + Text of 'a | + Antiq of Symbol_Pos.T list * Position.T | + Open of Position.T | + Close of Position.T + val is_antiq: 'a antiquote -> bool + val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list + val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list + val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) -> + Symbol_Pos.T list * Position.T -> 'a antiquote list +end; + +structure Antiquote: ANTIQUOTE = +struct + +(* datatype antiquote *) + +datatype 'a antiquote = + Text of 'a | + Antiq of Symbol_Pos.T list * Position.T | + Open of Position.T | + Close of Position.T; + +fun is_antiq (Text _) = false + | is_antiq _ = true; + + +(* check_nesting *) + +fun err_unbalanced pos = + error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); + +fun check_nesting antiqs = + let + fun check [] [] = () + | check [] (pos :: _) = err_unbalanced pos + | check (Open pos :: ants) ps = check ants (pos :: ps) + | check (Close pos :: _) [] = err_unbalanced pos + | check (Close _ :: ants) (_ :: ps) = check ants ps + | check (_ :: ants) ps = check ants ps; + in check antiqs [] end; + + +(* scan *) + +open Basic_Symbol_Pos; + +local + +val scan_txt = + $$$ "@" --| Scan.ahead (~$$$ "{") || + Scan.one (fn (s, _) => s <> "@" andalso s <> "\\" andalso s <> "\\" + andalso Symbol.is_regular s) >> single; + +val scan_ant = + Symbol_Pos.scan_quoted || + Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; + +val scan_antiq = + Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- + Symbol_Pos.!!! "missing closing brace of antiquotation" + (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) + >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2))); + +val scan_open = Symbol_Pos.scan_pos --| $$$ "\\"; +val scan_close = Symbol_Pos.scan_pos --| $$$ "\\"; + +in + +fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x; +val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat); + +end; + + +(* read *) + +fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos + | report_antiq _ = (); + +fun read _ ([], _) = [] + | read scanner (syms, pos) = + (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of + SOME xs => (List.app report_antiq xs; check_nesting xs; xs) + | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); + +end; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/General/symbol_pos.ML Thu Mar 19 22:05:37 2009 +0100 @@ -20,7 +20,11 @@ val is_eof: T -> bool val stopper: T Scan.stopper val !!! : string -> (T list -> 'a) -> T list -> 'a + val change_prompt: ('a -> 'b) -> 'a -> 'b val scan_pos: T list -> Position.T * T list + val scan_string: T list -> (Position.T * (T list * Position.T)) * T list + val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list + val scan_quoted: T list -> T list * T list val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> T list -> T list * T list val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> @@ -83,12 +87,44 @@ (case msg of NONE => "" | SOME s => "\n" ^ s); in Scan.!! err scan end; +fun change_prompt scan = Scan.prompt "# " scan; + fun $$$ s = Scan.one (fn x => symbol x = s) >> single; fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos); +(* Isabelle strings *) + +local + +val char_code = + Scan.one (Symbol.is_ascii_digit o symbol) -- + Scan.one (Symbol.is_ascii_digit o symbol) -- + Scan.one (Symbol.is_ascii_digit o symbol) :|-- + (fn (((a, pos), (b, _)), (c, _)) => + let val (n, _) = Library.read_int [a, b, c] + in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end); + +fun scan_str q = + $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) || + Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single; + +fun scan_strs q = + (scan_pos --| $$$ q) -- !!! "missing quote at end of string" + (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos))); + +in + +val scan_string = scan_strs "\""; +val scan_alt_string = scan_strs "`"; + +val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2; + +end; + + (* ML-style comments *) local @@ -99,7 +135,7 @@ Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) || Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single; -val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat); +val scan_body = change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat)); in diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/IsaMakefile Thu Mar 19 22:05:37 2009 +0100 @@ -45,17 +45,17 @@ Concurrent/mailbox.ML Concurrent/par_list.ML \ Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \ Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \ - General/alist.ML General/balanced_tree.ML General/basics.ML \ - General/binding.ML General/buffer.ML General/file.ML \ - General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \ - General/long_name.ML General/markup.ML General/name_space.ML \ - General/ord_list.ML General/output.ML General/path.ML \ - General/position.ML General/pretty.ML General/print_mode.ML \ - General/properties.ML General/queue.ML General/scan.ML \ - General/secure.ML General/seq.ML General/source.ML General/stack.ML \ - General/symbol.ML General/symbol_pos.ML General/table.ML \ - General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \ - Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ + General/alist.ML General/antiquote.ML General/balanced_tree.ML \ + General/basics.ML General/binding.ML General/buffer.ML \ + General/file.ML General/graph.ML General/heap.ML General/integer.ML \ + General/lazy.ML General/long_name.ML General/markup.ML \ + General/name_space.ML General/ord_list.ML General/output.ML \ + General/path.ML General/position.ML General/pretty.ML \ + General/print_mode.ML General/properties.ML General/queue.ML \ + General/scan.ML General/secure.ML General/seq.ML General/source.ML \ + General/stack.ML General/symbol.ML General/symbol_pos.ML \ + General/table.ML General/url.ML General/xml.ML General/yxml.ML \ + Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/ROOT.ML Thu Mar 19 22:05:37 2009 +0100 @@ -24,7 +24,6 @@ use "outer_parse.ML"; use "value_parse.ML"; use "args.ML"; -use "antiquote.ML"; use "../ML/ml_context.ML"; (*theory sources*) diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/antiquote.ML --- a/src/Pure/Isar/antiquote.ML Thu Mar 19 08:13:10 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,109 +0,0 @@ -(* Title: Pure/Isar/antiquote.ML - Author: Markus Wenzel, TU Muenchen - -Text with antiquotations of inner items (terms, types etc.). -*) - -signature ANTIQUOTE = -sig - datatype antiquote = - Text of string | Antiq of Symbol_Pos.T list * Position.T | - Open of Position.T | Close of Position.T - val is_antiq: antiquote -> bool - val read: Symbol_Pos.T list * Position.T -> antiquote list - val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) -> - Symbol_Pos.T list * Position.T -> 'a -end; - -structure Antiquote: ANTIQUOTE = -struct - -(* datatype antiquote *) - -datatype antiquote = - Text of string | - Antiq of Symbol_Pos.T list * Position.T | - Open of Position.T | - Close of Position.T; - -fun is_antiq (Text _) = false - | is_antiq _ = true; - - -(* check_nesting *) - -fun err_unbalanced pos = - error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); - -fun check_nesting antiqs = - let - fun check [] [] = () - | check [] (pos :: _) = err_unbalanced pos - | check (Open pos :: ants) ps = check ants (pos :: ps) - | check (Close pos :: _) [] = err_unbalanced pos - | check (Close _ :: ants) (_ :: ps) = check ants ps - | check (_ :: ants) ps = check ants ps; - in check antiqs [] end; - - -(* scan_antiquote *) - -open Basic_Symbol_Pos; -structure T = OuterLex; - -local - -val scan_txt = - $$$ "@" --| Scan.ahead (~$$$ "{") || - Scan.one (fn (s, _) => s <> "@" andalso s <> "\\" andalso s <> "\\" - andalso Symbol.is_regular s) >> single; - -val scan_ant = - T.scan_quoted || - Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; - -val scan_antiq = - Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- - T.!!! "missing closing brace of antiquotation" - (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) - >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2))); - -in - -val scan_antiquote = - (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) || - scan_antiq || - Symbol_Pos.scan_pos --| $$$ "\\" >> Open || - Symbol_Pos.scan_pos --| $$$ "\\" >> Close); - -end; - - -(* read *) - -fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos - | report_antiq _ = (); - -fun read ([], _) = [] - | read (syms, pos) = - (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of - SOME xs => (List.app report_antiq xs; check_nesting xs; xs) - | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); - - -(* read_antiq *) - -fun read_antiq lex scan (syms, pos) = - let - fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^ - "@{" ^ Symbol_Pos.content syms ^ "}"); - - val res = - Source.of_list syms - |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) - |> T.source_proper - |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE - |> Source.exhaust; - in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end; - -end; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/class.ML Thu Mar 19 22:05:37 2009 +0100 @@ -236,7 +236,7 @@ thy |> Sign.declare_const [] ((b, ty0), syn) |> snd - |> pair ((Binding.name_of b, ty), (c, ty')) + |> pair ((Name.of_binding b, ty), (c, ty')) end; in thy diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/constdefs.ML Thu Mar 19 22:05:37 2009 +0100 @@ -36,7 +36,7 @@ val prop = prep_prop var_ctxt raw_prop; val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop)); val _ = - (case Option.map Binding.name_of d of + (case Option.map Name.of_binding d of NONE => () | SOME c' => if c <> c' then diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/element.ML Thu Mar 19 22:05:37 2009 +0100 @@ -96,7 +96,7 @@ fun map_ctxt {binding, typ, term, pattern, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => - (Binding.name_of (binding (Binding.name x)), typ T))) + (Name.of_binding (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/expression.ML Thu Mar 19 22:05:37 2009 +0100 @@ -125,8 +125,8 @@ val (implicit, expr') = params_expr expr; - val implicit' = map (#1 #> Binding.name_of) implicit; - val fixed' = map (#1 #> Binding.name_of) fixed; + val implicit' = map (#1 #> Name.of_binding) implicit; + val fixed' = map (#1 #> Name.of_binding) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] @@ -352,7 +352,7 @@ fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) = let val (parm_names, parm_types) = Locale.params_of thy loc |> - map_split (fn (b, SOME T, _) => (Binding.name_of b, T)) + map_split (fn (b, SOME T, _) => (Name.of_binding b, T)) (*FIXME return value of Locale.params_of has strange type*) val inst' = prep_inst ctxt parm_names inst; val parm_types' = map (TypeInfer.paramify_vars o @@ -386,7 +386,7 @@ prep_concl raw_concl (insts', elems, ctxt5); (* Retrieve parameter types *) - val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes) + val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes) | _ => fn ps => ps) (Fixes fors :: elems') []; val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; val parms = xs ~~ Ts; (* params from expression and elements *) diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/local_defs.ML Thu Mar 19 22:05:37 2009 +0100 @@ -90,7 +90,7 @@ let val ((bvars, mxs), specs) = defs |> split_list |>> split_list; val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; - val xs = map Binding.name_of bvars; + val xs = map Name.of_binding bvars; val names = map2 Thm.def_binding_optional bvars bfacts; val eqs = mk_def ctxt (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/locale.ML Thu Mar 19 22:05:37 2009 +0100 @@ -181,7 +181,7 @@ fun axioms_of thy = #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> - map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph); + map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph); fun specification_of thy = #spec o the_locale thy; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/obtain.ML Thu Mar 19 22:05:37 2009 +0100 @@ -119,7 +119,7 @@ (*obtain vars*) val (vars, vars_ctxt) = prep_vars raw_vars ctxt; val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; - val xs = map (Binding.name_of o #1) vars; + val xs = map (Name.of_binding o #1) vars; (*obtain asms*) val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); @@ -258,7 +258,7 @@ fun inferred_type (binding, _, mx) ctxt = let - val x = Binding.name_of binding; + val x = Name.of_binding binding; val (T, ctxt') = ProofContext.inferred_param x ctxt in ((x, T, mx), ctxt') end; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/outer_lex.ML --- a/src/Pure/Isar/outer_lex.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/outer_lex.ML Thu Mar 19 22:05:37 2009 +0100 @@ -51,13 +51,14 @@ val closure: token -> token val ident_or_symbolic: string -> bool val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a - val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) -> (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) -> Position.T -> (Symbol.symbol, 'a) Source.source -> (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source + val read_antiq: Scan.lexicon -> (token list -> 'a * token list) -> + Symbol_Pos.T list * Position.T -> 'a end; structure OuterLex: OUTER_LEX = @@ -263,8 +264,6 @@ fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg); -fun change_prompt scan = Scan.prompt "# " scan; - (* scan symbolic idents *) @@ -286,36 +285,6 @@ | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s; -(* scan strings *) - -local - -val char_code = - Scan.one (Symbol.is_ascii_digit o symbol) -- - Scan.one (Symbol.is_ascii_digit o symbol) -- - Scan.one (Symbol.is_ascii_digit o symbol) :|-- - (fn (((a, pos), (b, _)), (c, _)) => - let val (n, _) = Library.read_int [a, b, c] - in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end); - -fun scan_str q = - $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) || - Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single; - -fun scan_strs q = - (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string" - (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos))); - -in - -val scan_string = scan_strs "\""; -val scan_alt_string = scan_strs "`"; - -val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2; - -end; - - (* scan verbatim text *) val scan_verb = @@ -324,7 +293,8 @@ val scan_verbatim = (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text" - (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos))); + (Symbol_Pos.change_prompt + ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos))); (* scan space *) @@ -346,7 +316,7 @@ val scan_malformed = $$$ Symbol.malformed |-- - change_prompt (Scan.many (Symbol.is_regular o symbol)) + Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol)) --| Scan.option ($$$ Symbol.end_malformed); @@ -366,8 +336,8 @@ Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot); fun scan (lex1, lex2) = !!! "bad input" - (scan_string >> token_range String || - scan_alt_string >> token_range AltString || + (Symbol_Pos.scan_string >> token_range String || + Symbol_Pos.scan_alt_string >> token_range AltString || scan_verbatim >> token_range Verbatim || scan_comment >> token_range Comment || scan_space >> token Space || @@ -401,4 +371,20 @@ end; + +(* read_antiq *) + +fun read_antiq lex scan (syms, pos) = + let + fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^ + "@{" ^ Symbol_Pos.content syms ^ "}"); + + val res = + Source.of_list syms + |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) + |> source_proper + |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE + |> Source.exhaust; + in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end; + end; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 19 22:05:37 2009 +0100 @@ -1003,7 +1003,7 @@ fun prep_vars prep_typ internal = fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt => let - val raw_x = Binding.name_of raw_b; + val raw_x = Name.of_binding raw_b; val (x, mx) = Syntax.const_mixfix raw_x raw_mx; val _ = Syntax.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ quote x); @@ -1113,7 +1113,7 @@ fun gen_fixes prep raw_vars ctxt = let val (vars, _) = prep raw_vars ctxt; - val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt; + val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt; val ctxt'' = ctxt' |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Isar/specification.ML Thu Mar 19 22:05:37 2009 +0100 @@ -161,7 +161,7 @@ fun gen_axioms do_print prep raw_vars raw_specs thy = let val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy); - val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars; + val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars; (*consts*) val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars; @@ -171,7 +171,7 @@ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => fold_map Thm.add_axiom (map (apfst (fn a => Binding.map_name (K a) b)) - (PureThy.name_multi (Binding.name_of b) (map subst props))) + (PureThy.name_multi (Name.of_binding b) (map subst props))) #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))); (*facts*) @@ -198,7 +198,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Binding.name_of b; + val y = Name.of_binding b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -234,7 +234,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Binding.name_of b; + val y = Name.of_binding b; val _ = x = y orelse error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -292,10 +292,10 @@ | Element.Obtains obtains => let val case_names = obtains |> map_index (fn (i, (b, _)) => - if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b); + if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b); val constraints = obtains |> map (fn (_, (vars, _)) => Element.Constrains - (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE))); + (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE))); val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; @@ -305,7 +305,7 @@ fun assume_case ((name, (vars, _)), asms) ctxt' = let val bs = map fst vars; - val xs = map Binding.name_of bs; + val xs = map Name.of_binding bs; val props = map fst asms; val (Ts, _) = ctxt' |> fold Variable.declare_term props diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/ML/ml_context.ML Thu Mar 19 22:05:37 2009 +0100 @@ -183,6 +183,7 @@ local structure P = OuterParse; +structure T = OuterLex; val antiq = P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof) @@ -193,7 +194,7 @@ fun eval_antiquotes (txt, pos) opt_context = let val syms = Symbol_Pos.explode (txt, pos); - val ants = Antiquote.read (syms, pos); + val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos); val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context; val ((ml_env, ml_body), opt_ctxt') = if not (exists Antiquote.is_antiq ants) @@ -209,11 +210,12 @@ val lex = #1 (OuterKeyword.get_lexicons ()); fun no_decl _ = ("", ""); - fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state) + fun expand (Antiquote.Text tok) state = + (K ("", Symbol.escape (ML_Lex.content_of tok)), state) | expand (Antiquote.Antiq x) (scope, background) = let val context = Stack.top scope; - val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context; + val (f, context') = antiquotation (T.read_antiq lex antiq x) context; val (decl, background') = f {background = background, struct_name = struct_name}; in (decl, (Stack.map_top (K context') scope, background')) end | expand (Antiquote.Open _) (scope, background) = diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/ML/ml_lex.ML Thu Mar 19 22:05:37 2009 +0100 @@ -17,9 +17,11 @@ val kind_of: token -> token_kind val content_of: token -> string val keywords: string list + val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list val source: (Symbol.symbol, 'a) Source.source -> (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source + val tokenize: string -> token list end; structure ML_Lex: ML_LEX = @@ -161,7 +163,8 @@ Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]); val scan_str = - Scan.one (fn (s, _) => Symbol.is_printable s andalso s <> "\"" andalso s <> "\\") >> single || + Scan.one (fn (s, _) => Symbol.is_regular s andalso Symbol.is_printable s + andalso s <> "\"" andalso s <> "\\") >> single || $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; @@ -183,9 +186,9 @@ local -fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss)); +fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); -val scan = !!! "bad input" +val scan_ml = (scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || @@ -205,9 +208,13 @@ in +val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text; + fun source src = Symbol_Pos.source (Position.line 1) src - |> Source.source Symbol_Pos.stopper (Scan.bulk scan) (SOME (false, recover)); + |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover)); + +val tokenize = Source.of_string #> source #> Source.exhaust; end; diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Thy/latex.ML Thu Mar 19 22:05:37 2009 +0100 @@ -88,7 +88,7 @@ val output_syms = output_symbols o Symbol.explode; val output_syms_antiq = - (fn Antiquote.Text s => output_syms s + (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) | Antiquote.Antiq (ss, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss)) | Antiquote.Open _ => "{\\isaantiqopen}" @@ -117,7 +117,7 @@ else if T.is_kind T.Verbatim tok then let val (txt, pos) = T.source_position_of tok; - val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); + val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); val out = implode (map output_syms_antiq ants); in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end else output_syms s diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/Thy/thy_output.ML Thu Mar 19 22:05:37 2009 +0100 @@ -147,16 +147,16 @@ fun eval_antiquote lex state (txt, pos) = let - fun expand (Antiquote.Text s) = s + fun expand (Antiquote.Text ss) = Symbol_Pos.content ss | expand (Antiquote.Antiq x) = - let val (opts, src) = Antiquote.read_antiq lex antiq x in + let val (opts, src) = T.read_antiq lex antiq x in options opts (fn () => command src state) (); (*preview errors!*) PrintMode.with_modes (! modes @ Latex.modes) (Output.no_warnings (options opts (fn () => command src state))) () end | expand (Antiquote.Open _) = "" | expand (Antiquote.Close _) = ""; - val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); + val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); in if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos) diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/mk --- a/src/Pure/mk Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/mk Thu Mar 19 22:05:37 2009 +0100 @@ -91,6 +91,7 @@ -e "val ml_system = \"$ML_SYSTEM\";" \ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "use\"$COMPAT\" handle _ => exit 1;" \ + -e "structure Isar = struct fun main () = () end;" \ -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 RC="$?" elif [ -n "$RAW_SESSION" ]; then diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/name.ML --- a/src/Pure/name.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/name.ML Thu Mar 19 22:05:37 2009 +0100 @@ -8,6 +8,7 @@ sig val uu: string val aT: string + val of_binding: binding -> string val bound: int -> string val is_bound: string -> bool val internal: string -> string @@ -41,6 +42,11 @@ (** special variable names **) +(* checked binding *) + +val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming; + + (* encoded bounds *) (*names for numbered variables -- diff -r eb827cd69fd3 -r 4216e9c70cfe src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/Pure/sign.ML Thu Mar 19 22:05:37 2009 +0100 @@ -434,7 +434,7 @@ fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) => let - val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn; + val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn; val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types; val tags = [(Markup.theory_nameN, Context.theory_name thy)]; val tsig' = fold (Type.add_type naming tags) decls tsig; @@ -445,7 +445,7 @@ fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) => let - val syn' = Syntax.update_consts (map Binding.name_of ns) syn; + val syn' = Syntax.update_consts (map Name.of_binding ns) syn; val tsig' = fold (Type.add_nonterminal naming []) ns tsig; in (naming, syn', tsig', consts) end); @@ -456,7 +456,7 @@ thy |> map_sign (fn (naming, syn, tsig, consts) => let val ctxt = ProofContext.init thy; - val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn; + val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn; val b = Binding.map_name (Syntax.type_name mx) a; val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs)) handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b)); @@ -504,10 +504,10 @@ val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt; fun prep (raw_b, raw_T, raw_mx) = let - val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx; + val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx; val b = Binding.map_name (K mx_name) raw_b; val c = full_name thy b; - val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b; + val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b)); val T' = Logic.varifyT T; @@ -568,7 +568,7 @@ fun primitive_class (bclass, classes) thy = thy |> map_sign (fn (naming, syn, tsig, consts) => let - val syn' = Syntax.update_consts [Binding.name_of bclass] syn; + val syn' = Syntax.update_consts [Name.of_binding bclass] syn; val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig; in (naming, syn', tsig', consts) end) |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; diff -r eb827cd69fd3 -r 4216e9c70cfe src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Mar 19 08:13:10 2009 -0700 +++ b/src/ZF/Tools/inductive_package.ML Thu Mar 19 22:05:37 2009 +0100 @@ -231,12 +231,12 @@ if !Ind_Syntax.trace then print_tac "The type-checking subgoal:" else all_tac, REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks - ORELSE' eresolve_tac (asm_rl::@{thm PartE}::@{thm SigmaE2}:: + ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} :: type_elims) ORELSE' hyp_subst_tac)), if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:" else all_tac, - DEPTH_SOLVE (swap_res_tac (@{thm SigmaI}::@{thm subsetI}::type_intrs) 1)]; + DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)]; (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*) val mk_disj_rls = BalancedTree.accesses