--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon May 20 20:54:11 2013 +0200
@@ -2695,8 +2695,8 @@
val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
- K (mk_in_bd_tac lthy (* FIXME proper context!? *)
- (nth isNode_hsets (i - 1)) isNode_hsets carT_def
+ (fn {context = ctxt, prems = _} =>
+ mk_in_bd_tac ctxt (nth isNode_hsets (i - 1)) isNode_hsets carT_def
card_of_carT mor_image Rep_inverse mor_hsets
sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
ks isNode_hset_thmss carT_defs card_of_carT_thms
--- a/src/HOL/BNF/Tools/bnf_util.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Mon May 20 20:54:11 2013 +0200
@@ -167,9 +167,9 @@
val standard_binding: binding
val equal_binding: binding
- val parse_binding: Token.T list -> binding * Token.T list
- val parse_binding_colon: Token.T list -> binding * Token.T list
- val parse_opt_binding_colon: Token.T list -> binding * Token.T list
+ val parse_binding: binding parser
+ val parse_binding_colon: binding parser
+ val parse_opt_binding_colon: binding parser
val typedef: binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
--- a/src/HOL/Decision_Procs/Approximation.thy Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon May 20 20:54:11 2013 +0200
@@ -3487,7 +3487,7 @@
(@{cpat "?prec::nat"}, p),
(@{cpat "?ss::nat list"}, s)])
@{thm "approx_form"}) i
- THEN simp_tac @{context} i) st
+ THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
end
| SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
@@ -3531,7 +3531,7 @@
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
rtac @{thm impI}] i)
- THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
THEN DETERM (TRY (filter_prems_tac (K false) i))
THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
@@ -3621,33 +3621,33 @@
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> snd
- fun apply_tactic context term tactic = cterm_of context term
+ fun apply_tactic ctxt term tactic =
+ cterm_of (Proof_Context.theory_of ctxt) term
|> Goal.init
|> SINGLE tactic
|> the |> prems_of |> hd
- fun prepare_form context term = apply_tactic context term (
+ fun prepare_form ctxt term = apply_tactic ctxt term (
REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
- THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) @{context} 1
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
THEN DETERM (TRY (filter_prems_tac (K false) 1)))
- fun reify_form context term = apply_tactic context term
- (Reflection.gen_reify_tac @{context} form_equations NONE 1)
+ fun reify_form ctxt term = apply_tactic ctxt term
+ (Reflection.gen_reify_tac ctxt form_equations NONE 1)
fun approx_form prec ctxt t =
realify t
- |> prepare_form (Proof_Context.theory_of ctxt)
- |> (fn arith_term =>
- reify_form (Proof_Context.theory_of ctxt) arith_term
- |> HOLogic.dest_Trueprop |> dest_interpret_form
- |> (fn (data, xs) =>
- mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
- (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
- |> approximate ctxt
- |> HOLogic.dest_list
- |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
- |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
- |> foldr1 HOLogic.mk_conj))
+ |> prepare_form ctxt
+ |> (fn arith_term => reify_form ctxt arith_term
+ |> HOLogic.dest_Trueprop |> dest_interpret_form
+ |> (fn (data, xs) =>
+ mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
+ (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
+ |> approximate ctxt
+ |> HOLogic.dest_list
+ |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
+ |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
+ |> foldr1 HOLogic.mk_conj))
fun approx_arith prec ctxt t = realify t
|> Reflection.gen_reify ctxt form_equations
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon May 20 20:54:11 2013 +0200
@@ -872,6 +872,7 @@
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
+ val ss = simpset_of @{context}
in
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
Const(@{const_name Orderings.less},_)$a$b =>
@@ -880,7 +881,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| Const(@{const_name Orderings.less_eq},_)$a$b =>
@@ -889,7 +890,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
@@ -899,7 +900,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
--- a/src/HOL/Prolog/prolog.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Prolog/prolog.ML Mon May 20 20:54:11 2013 +0200
@@ -65,7 +65,8 @@
@{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
@{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
@{thm imp_conjR}, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
- @{thm imp_all}]; (* "((!x. D) :- G) = (!x. D :- G)" *)
+ @{thm imp_all}] (* "((!x. D) :- G) = (!x. D :- G)" *)
+ |> simpset_of;
(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
@@ -114,7 +115,7 @@
rtac allI, (* "(!!x. P x) ==> ! x. P x" *)
rtac exI, (* "P x ==> ? x. P x" *)
rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *)
- asm_full_simp_tac atomize_ss THEN' (* atomize the asms *)
+ asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN' (* atomize the asms *)
(REPEAT_DETERM o (etac conjE)) (* split the asms *)
])
ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*)
--- a/src/HOL/Tools/Function/partial_function.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon May 20 20:54:11 2013 +0200
@@ -255,11 +255,11 @@
val unfold =
(cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
OF [mono_thm, f_def])
- |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy) 1);
+ |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
val mk_raw_induct =
mk_curried_induct args args_ctxt (cert curry) (cert uncurry)
- #> singleton (Variable.export args_ctxt lthy)
+ #> singleton (Variable.export args_ctxt lthy')
#> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [mono_thm, f_def])
#> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
--- a/src/HOL/Tools/groebner.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Tools/groebner.ML Mon May 20 20:54:11 2013 +0200
@@ -1002,6 +1002,8 @@
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
+
+ val claset = claset_of @{context}
in
fun ideal_tac add_ths del_ths ctxt =
presimplify ctxt add_ths del_ths
@@ -1023,10 +1025,10 @@
THEN ring_tac add_ths del_ths ctxt 1
end
in
- clarify_tac @{context} i
+ clarify_tac (put_claset claset ctxt) i
THEN Object_Logic.full_atomize_tac i
THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
- THEN clarify_tac @{context} i
+ THEN clarify_tac (put_claset claset ctxt) i
THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
THEN SUBPROOF poly_exists_tac ctxt i
end
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon May 20 20:54:11 2013 +0200
@@ -722,8 +722,8 @@
@{thm rename_guarantees_eq_rename_inv},
@{thm bij_imp_bij_inv}, @{thm surj_rename},
@{thm inv_inv_eq}]) 1,
- asm_simp_tac (* FIXME ctxt !!? *)
- (@{context} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
+ asm_simp_tac
+ (ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
*}
method_setup rename_client_map = {*
--- a/src/Pure/Concurrent/time_limit.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML Mon May 20 20:54:11 2013 +0200
@@ -32,8 +32,7 @@
in
if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
then raise TimeOut
- else if Exn.is_interrupt_exn test then Exn.interrupt ()
- else Exn.release result
+ else (Exn.release test; Exn.release result)
end);
end;
--- a/src/Pure/System/session.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/System/session.ML Mon May 20 20:54:11 2013 +0200
@@ -54,7 +54,6 @@
Present.finish ();
Keyword.status ();
Outer_Syntax.check_syntax ();
- Options.reset_default ();
Future.shutdown ();
Event_Timer.shutdown ();
session_finished := true);
--- a/src/Pure/System/session.scala Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/System/session.scala Mon May 20 20:54:11 2013 +0200
@@ -177,6 +177,7 @@
version: Document.Version)
private case class Messages(msgs: List[Isabelle_Process.Message])
private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
+ private case class Update_Options(options: Options)
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
@@ -415,8 +416,10 @@
receiver.cancel()
reply(())
- case Session.Global_Options(options) if prover.isDefined =>
+ case Update_Options(options) if prover.isDefined =>
if (is_ready) prover.get.options(options)
+ global_options.event(Session.Global_Options(options))
+ reply(())
case Cancel_Execution if prover.isDefined =>
prover.get.cancel_execution()
@@ -470,13 +473,11 @@
def start(args: List[String])
{
- global_options += session_actor
session_actor ! Start(args)
}
def stop()
{
- global_options -= session_actor
commands_changed_buffer !? Stop
change_parser !? Stop
session_actor !? Stop
@@ -487,6 +488,9 @@
def update(edits: List[Document.Edit_Text])
{ if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
+ def update_options(options: Options)
+ { session_actor !? Update_Options(options) }
+
def dialog_result(id: Document.ID, serial: Long, result: String)
{ session_actor ! Session.Dialog_Result(id, serial, result) }
}
--- a/src/Pure/build Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/build Mon May 20 20:54:11 2013 +0200
@@ -80,6 +80,7 @@
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
-e "Command_Line.tool0 Session.finish;" \
+ -e "Options.reset_default ();" \
-q -w RAW_ML_SYSTEM "$OUTPUT"
fi
fi
--- a/src/Pure/raw_simplifier.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/raw_simplifier.ML Mon May 20 20:54:11 2013 +0200
@@ -510,10 +510,6 @@
fun add_prems ths =
map_simpset1 (fn (rules, prems, bounds, depth) => (rules, ths @ prems, bounds, depth));
-fun activate_context thy ctxt = ctxt (* FIXME ?? *)
- |> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
- |> Context_Position.set_visible false;
-
(* maintain simp rules *)
@@ -545,7 +541,6 @@
fun decomp_simp thm =
let
- val thy = Thm.theory_of_thm thm;
val prop = Thm.prop_of thm;
val prems = Logic.strip_imp_prems prop;
val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
@@ -557,12 +552,12 @@
var_perm (term_of elhs, erhs) andalso
not (term_of elhs aconv erhs) andalso
not (is_Var (term_of elhs));
- in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
+ in (prems, term_of lhs, elhs, term_of rhs, perm) end;
end;
fun decomp_simp' thm =
- let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
+ let val (_, lhs, _, rhs, _) = decomp_simp thm in
if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
else (lhs, rhs)
end;
@@ -572,13 +567,13 @@
(case mk_eq_True ctxt thm of
NONE => []
| SOME eq_True =>
- let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
+ let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end)
end;
(*create the rewrite rule and possibly also the eq_True variant,
in case there are extra vars on the rhs*)
-fun rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm2) =
+fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 =
let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
if rewrite_rule_extra_vars [] lhs rhs then
mk_eq_True ctxt (thm2, name) @ [rrule]
@@ -586,18 +581,18 @@
end;
fun mk_rrule ctxt (thm, name) =
- let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
+ let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
else
(*weak test for loops*)
if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
then mk_eq_True ctxt (thm, name)
- else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
+ else rrule_eq_True ctxt thm name lhs elhs rhs thm
end;
fun orient_rrule ctxt (thm, name) =
let
- val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
+ val (prems, lhs, elhs, rhs, perm) = decomp_simp thm;
val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt;
in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
@@ -608,9 +603,9 @@
(case mk_sym ctxt thm of
NONE => []
| SOME thm' =>
- let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
- in rrule_eq_True (thm', name, lhs', elhs', rhs', ctxt, thm) end)
- else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
+ let val (_, lhs', elhs', rhs', _) = decomp_simp thm'
+ in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end)
+ else rrule_eq_True ctxt thm name lhs elhs rhs thm
end;
fun extract_rews (ctxt, thms) =
@@ -886,7 +881,7 @@
(* mk_procrule *)
fun mk_procrule ctxt thm =
- let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
+ let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in
if rewrite_rule_extra_vars prems lhs rhs
then (cond_warn_thm ctxt (fn () => "Extra vars on rhs:") thm; [])
else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
@@ -934,7 +929,7 @@
IMPORTANT: rewrite rules must not introduce new Vars or TVars!
*)
-fun rewritec (prover, thyt, maxt) ctxt t =
+fun rewritec (prover, maxt) ctxt t =
let
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt;
val eta_thm = Thm.eta_conversion t;
@@ -1007,7 +1002,7 @@
fun proc_rews [] = NONE
| proc_rews (Proc {name, proc, lhs, ...} :: ps) =
- if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
+ if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
(debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
case proc ctxt eta_t' of
NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
@@ -1063,20 +1058,20 @@
fun transitive2 thm = transitive1 (SOME thm);
fun transitive3 thm = transitive1 thm o SOME;
-fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
+fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
let
fun botc skel ctxt t =
if is_Var skel then NONE
else
(case subc skel ctxt t of
some as SOME thm1 =>
- (case rewritec (prover, thy, maxidx) ctxt (Thm.rhs_of thm1) of
+ (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
SOME (thm2, skel2) =>
transitive2 (Thm.transitive thm1 thm2)
(botc skel2 ctxt (Thm.rhs_of thm2))
| NONE => some)
| NONE =>
- (case rewritec (prover, thy, maxidx) ctxt t of
+ (case rewritec (prover, maxidx) ctxt t of
SOME (thm2, skel2) => transitive2 thm2
(botc skel2 ctxt (Thm.rhs_of thm2))
| NONE => NONE))
@@ -1197,7 +1192,7 @@
Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
val dprem = Option.map (disch false prem)
in
- (case rewritec (prover, thy, maxidx) ctxt' concl' of
+ (case rewritec (prover, maxidx) ctxt' concl' of
NONE => rebuild prems concl' rrss asms ctxt (dprem eq)
| SOME (eq', _) => transitive2 (fold (disch false)
prems (the (transitive3 (dprem eq) eq')))
@@ -1305,10 +1300,18 @@
fun rewrite_cterm mode prover raw_ctxt raw_ct =
let
- val thy = Thm.theory_of_cterm raw_ct;
+ val ctxt =
+ raw_ctxt
+ |> Context_Position.set_visible false
+ |> inc_simp_depth;
+ val thy = Proof_Context.theory_of ctxt;
+
val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
val {maxidx, ...} = Thm.rep_cterm ct;
- val ctxt = inc_simp_depth (activate_context thy raw_ctxt);
+ val _ =
+ Theory.subthy (theory_of_cterm ct, thy) orelse
+ raise CTERM ("rewrite_cterm: bad background theory", [ct]);
+
val depth = simp_depth ctxt;
val _ =
if depth mod 20 = 0 then
@@ -1316,7 +1319,7 @@
else ();
val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
val _ = check_bounds ctxt ct;
- in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ctxt ct end;
+ in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
val simple_prover =
SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
--- a/src/Pure/tactic.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/tactic.ML Mon May 20 20:54:11 2013 +0200
@@ -85,8 +85,9 @@
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic ctxt tac rl =
let
+ val thy = Proof_Context.theory_of ctxt;
val ctxt' = Variable.declare_thm rl ctxt;
- val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
+ val ((_, [st]), ctxt'') = Variable.import true [Thm.transfer thy rl] ctxt';
in
(case Seq.pull (tac st) of
NONE => raise THM ("rule_by_tactic", 0, [rl])
--- a/src/Tools/Code/code_printer.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/Code/code_printer.ML Mon May 20 20:54:11 2013 +0200
@@ -101,8 +101,8 @@
| Complex_const_syntax of activated_complex_const_syntax
type tyco_syntax
val requires_args: const_syntax -> int
- val parse_const_syntax: Token.T list -> const_syntax * Token.T list
- val parse_tyco_syntax: Token.T list -> tyco_syntax * Token.T list
+ val parse_const_syntax: const_syntax parser
+ val parse_tyco_syntax: tyco_syntax parser
val plain_const_syntax: string -> const_syntax
val simple_const_syntax: simple_const_syntax -> const_syntax
val complex_const_syntax: complex_const_syntax -> const_syntax
--- a/src/Tools/jEdit/src/active.scala Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala Mon May 20 20:54:11 2013 +0200
@@ -77,14 +77,10 @@
else text_area.setSelectedText(text)
}
+ case Protocol.Dialog(id, serial, result) =>
+ model.session.dialog_result(id, serial, result)
+
case _ =>
- // FIXME pattern match problem in scala-2.9.2 (!??)
- elem match {
- case Protocol.Dialog(id, serial, result) =>
- model.session.dialog_result(id, serial, result)
-
- case _ =>
- }
}
}
}
--- a/src/Tools/jEdit/src/plugin.scala Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon May 20 20:54:11 2013 +0200
@@ -196,7 +196,7 @@
}
case Session.Ready =>
- PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+ PIDE.session.update_options(PIDE.options.value)
PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
Swing_Thread.later { delay_load.invoke() }
@@ -270,7 +270,7 @@
}
case msg: PropertiesChanged =>
- PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+ PIDE.session.update_options(PIDE.options.value)
case _ =>
}
--- a/src/Tools/jEdit/src/rendering.scala Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon May 20 20:54:11 2013 +0200
@@ -481,17 +481,12 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
- // FIXME pattern match problem in scala-2.9.2 (!??)
- elem match {
- case Protocol.Dialog(_, serial, result) =>
- command_state.results.get(serial) match {
- case Some(Protocol.Dialog_Result(res)) if res == result =>
- (None, Some(active_result_color))
- case _ =>
- (None, Some(active_color))
- }
- case _ => acc
+ case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+ command_state.results.get(serial) match {
+ case Some(Protocol.Dialog_Result(res)) if res == result =>
+ (None, Some(active_result_color))
+ case _ =>
+ (None, Some(active_color))
}
case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
(None, Some(active_color))
--- a/src/ZF/Tools/inductive_package.ML Mon May 20 16:12:33 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon May 20 20:54:11 2013 +0200
@@ -252,15 +252,15 @@
val dummy = writeln " Proving the elimination rule...";
(*Breaks down logical connectives in the monotonic function*)
- val basic_elim_tac =
+ fun basic_elim_tac ctxt =
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
- ORELSE' bound_hyp_subst_tac ctxt1))
+ ORELSE' bound_hyp_subst_tac ctxt))
THEN prune_params_tac
(*Mutual recursion: collapse references to Part(D,h)*)
THEN (PRIMITIVE (fold_rule part_rec_defs));
(*Elimination*)
- val elim = rule_by_tactic (Proof_Context.init_global thy1) basic_elim_tac
+ val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1)
(unfold RS Ind_Syntax.equals_CollectD)
(*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
Proposition A should have the form t:Si where Si is an inductive set*)
fun make_cases ctxt A =
rule_by_tactic ctxt
- (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac)
+ (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
(Thm.assume A RS elim)
|> Drule.export_without_context_open;