--- a/src/HOL/Nominal/nominal_induct.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Nov 04 13:52:19 2011 +0100
@@ -72,7 +72,7 @@
val ys =
if p < n then []
else map (tune o #1) (take (p - n) ps) @ xs;
- in Logic.list_rename_params (ys, prem) end;
+ in Logic.list_rename_params ys prem end;
fun rename_prems prop =
let val (As, C) = Logic.strip_horn prop
in Logic.list_implies (map rename As, C) end;
--- a/src/Pure/Isar/element.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/element.ML Fri Nov 04 13:52:19 2011 +0100
@@ -294,9 +294,9 @@
in proof after_qed' propss #> refine_witness #> Seq.hd end;
fun proof_local cmd goal_ctxt int after_qed' propss =
- Proof.map_context (K goal_ctxt)
- #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
- cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+ Proof.map_context (K goal_ctxt) #>
+ Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
+ cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
in
--- a/src/Pure/Isar/obtain.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/obtain.ML Fri Nov 04 13:52:19 2011 +0100
@@ -123,7 +123,8 @@
val xs = map (Variable.check_name o #1) vars;
(*obtain asms*)
- val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
+ val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
+ val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
val asm_props = maps (map fst) proppss;
val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
@@ -138,11 +139,11 @@
val that_name = if name = "" then thatN else name;
val that_prop =
- Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
- |> Library.curry Logic.list_rename_params xs;
+ Logic.list_rename_params xs
+ (Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)));
val obtain_prop =
- Logic.list_rename_params ([Auto_Bind.thesisN],
- Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
+ Logic.list_rename_params [Auto_Bind.thesisN]
+ (Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
fun after_qed _ =
Proof.local_qed (NONE, false)
@@ -153,6 +154,7 @@
state
|> Proof.enter_forward
|> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+ |> Proof.map_context bind_ctxt
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume
@@ -308,7 +310,7 @@
|> Proof.begin_block
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
- |> Proof.local_goal print_result (K I) (apsnd (rpair I))
+ |> Proof.local_goal print_result (K I) (pair o rpair I)
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
|> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
end;
--- a/src/Pure/Isar/parse.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/parse.ML Fri Nov 04 13:52:19 2011 +0100
@@ -322,7 +322,7 @@
val simple_fixes = and_list1 params >> flat;
val fixes =
- and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
+ and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
--- a/src/Pure/Isar/proof.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/proof.ML Fri Nov 04 13:52:19 2011 +0100
@@ -84,7 +84,7 @@
val apply_end: Method.text -> state -> state Seq.seq
val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
(theory -> 'a -> attribute) ->
- (context * 'b list -> context * (term list list * (context -> context))) ->
+ ('b list -> context -> (term list list * (context -> context)) * context) ->
string -> Method.text option -> (thm list list -> state -> state) ->
((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state
@@ -863,7 +863,7 @@
|> assert_forward_or_chain
|> enter_forward
|> open_block
- |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
+ |> map_context_result (prepp raw_propp);
val props = flat propss;
val vars = implicit_vars props;
@@ -938,9 +938,13 @@
(* global goals *)
-fun global_goal prepp before_qed after_qed propp ctxt =
- init ctxt
- |> generic_goal (prepp #> Proof_Context.auto_fixes) "" before_qed (K I, after_qed) propp;
+fun prepp_auto_fixes prepp args =
+ prepp args #>
+ (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
+
+fun global_goal prepp before_qed after_qed propp =
+ init #>
+ generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
val theorem = global_goal Proof_Context.bind_propp_schematic_i;
val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
--- a/src/Pure/Isar/proof_context.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 04 13:52:19 2011 +0100
@@ -93,22 +93,22 @@
val auto_bind_facts: term list -> Proof.context -> Proof.context
val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
val match_bind_i: bool -> (term list * term) list -> Proof.context -> term list * Proof.context
- val read_propp: Proof.context * (string * string list) list list
- -> Proof.context * (term * term list) list list
- val cert_propp: Proof.context * (term * term list) list list
- -> Proof.context * (term * term list) list list
- val read_propp_schematic: Proof.context * (string * string list) list list
- -> Proof.context * (term * term list) list list
- val cert_propp_schematic: Proof.context * (term * term list) list list
- -> Proof.context * (term * term list) list list
- val bind_propp: Proof.context * (string * string list) list list
- -> Proof.context * (term list list * (Proof.context -> Proof.context))
- val bind_propp_i: Proof.context * (term * term list) list list
- -> Proof.context * (term list list * (Proof.context -> Proof.context))
- val bind_propp_schematic: Proof.context * (string * string list) list list
- -> Proof.context * (term list list * (Proof.context -> Proof.context))
- val bind_propp_schematic_i: Proof.context * (term * term list) list list
- -> Proof.context * (term list list * (Proof.context -> Proof.context))
+ val read_propp: (string * string list) list list -> Proof.context ->
+ (term * term list) list list * Proof.context
+ val cert_propp: (term * term list) list list -> Proof.context ->
+ (term * term list) list list * Proof.context
+ val read_propp_schematic: (string * string list) list list -> Proof.context ->
+ (term * term list) list list * Proof.context
+ val cert_propp_schematic: (term * term list) list list -> Proof.context ->
+ (term * term list) list list * Proof.context
+ val bind_propp: (string * string list) list list -> Proof.context ->
+ (term list list * (Proof.context -> Proof.context)) * Proof.context
+ val bind_propp_i: (term * term list) list list -> Proof.context ->
+ (term list list * (Proof.context -> Proof.context)) * Proof.context
+ val bind_propp_schematic: (string * string list) list list -> Proof.context ->
+ (term list list * (Proof.context -> Proof.context)) * Proof.context
+ val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
+ (term list list * (Proof.context -> Proof.context)) * Proof.context
val fact_tac: thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
val get_fact: Proof.context -> Facts.ref -> thm list
@@ -124,7 +124,6 @@
(binding * typ option * mixfix) list * Proof.context
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
- val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val add_assms: Assumption.export ->
(Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
@@ -778,26 +777,26 @@
local
-fun prep_propp mode prep_props (context, args) =
+fun prep_propp mode prep_props args context =
let
fun prep (_, raw_pats) (ctxt, prop :: props) =
let val ctxt' = Variable.declare_term prop ctxt
in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end;
- val (propp, (context', _)) = (fold_map o fold_map) prep args
- (context, prep_props (set_mode mode context) (maps (map fst) args));
- in (context', propp) end;
+ val (propp, (context', _)) =
+ (fold_map o fold_map) prep args
+ (context, prep_props (set_mode mode context) (maps (map fst) args));
+ in (propp, context') end;
-fun gen_bind_propp mode parse_prop (ctxt, raw_args) =
+fun gen_bind_propp mode parse_prop raw_args ctxt =
let
- val (ctxt', args) = prep_propp mode parse_prop (ctxt, raw_args);
+ val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
val binds = flat (flat (map (map (simult_matches ctxt')) args));
val propss = map (map #1) args;
-
- (*generalize result: context evaluated now, binds added later*)
- val gen = Variable.exportT_terms ctxt' ctxt;
- fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
- in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
+ fun gen_binds ctxt0 = ctxt0
+ |> bind_terms (map #1 binds ~~
+ map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
+ in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
in
@@ -1038,9 +1037,6 @@
#> pair xs)
end;
-fun auto_fixes (ctxt, (propss, x)) =
- ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
-
(** assumptions **)
@@ -1050,7 +1046,7 @@
fun gen_assms prepp exp args ctxt =
let
val cert = Thm.cterm_of (theory_of ctxt);
- val (propss, ctxt1) = swap (prepp (ctxt, map snd args));
+ val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
val _ = Variable.warn_extra_tfrees ctxt ctxt1;
val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
in
@@ -1061,8 +1057,8 @@
in
-val add_assms = gen_assms (apsnd #1 o bind_propp);
-val add_assms_i = gen_assms (apsnd #1 o bind_propp_i);
+val add_assms = gen_assms bind_propp;
+val add_assms_i = gen_assms bind_propp_i;
end;
--- a/src/Pure/Isar/rule_cases.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/rule_cases.ML Fri Nov 04 13:52:19 2011 +0100
@@ -403,7 +403,7 @@
fun rename prem =
let val xs =
map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
- in Logic.list_rename_params (xs, prem) end;
+ in Logic.list_rename_params xs prem end;
fun rename_prems prop =
let val (As, C) = Logic.strip_horn prop
in Logic.list_implies (map rename As, C) end;
--- a/src/Pure/Isar/specification.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/Isar/specification.ML Fri Nov 04 13:52:19 2011 +0100
@@ -308,7 +308,7 @@
val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
- val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
+ val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
in ((prems, stmt, NONE), goal_ctxt) end
| Element.Obtains obtains =>
let
--- a/src/Pure/logic.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/logic.ML Fri Nov 04 13:52:19 2011 +0100
@@ -46,7 +46,7 @@
val name_arity: string * sort list * class -> string
val mk_arities: arity -> term list
val dest_arity: term -> string * sort list * class
- val unconstrainT: sort list -> term ->
+ val unconstrainT: sort list -> term ->
((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
val protectC: term
val protect: term -> term
@@ -68,8 +68,8 @@
val strip_params: term -> (string * typ) list
val has_meta_prems: term -> bool
val flatten_params: int -> term -> term
- val list_rename_params: string list * term -> term
- val assum_pairs: int * term -> (term*term)list
+ val list_rename_params: string list -> term -> term
+ val assum_pairs: int * term -> (term * term) list
val assum_problems: int * term -> (term -> term) * term list * term
val varifyT_global: typ -> typ
val unvarifyT_global: typ -> typ
@@ -453,11 +453,11 @@
end;
(*Makes parameters in a goal have the names supplied by the list cs.*)
-fun list_rename_params (cs, Const("==>", _) $ A $ B) =
- implies $ A $ list_rename_params (cs, B)
- | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
- a $ Abs(c, T, list_rename_params (cs, t))
- | list_rename_params (cs, B) = B;
+fun list_rename_params cs (Const ("==>", _) $ A $ B) =
+ implies $ A $ list_rename_params cs B
+ | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
+ a $ Abs (c, T, list_rename_params cs t)
+ | list_rename_params cs B = B;
--- a/src/Pure/simplifier.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/simplifier.ML Fri Nov 04 13:52:19 2011 +0100
@@ -184,9 +184,7 @@
lhss =
let
val lhss' = prep lthy lhss;
- val ctxt' = lthy
- |> fold Variable.declare_term lhss'
- |> fold Variable.auto_fixes lhss';
+ val ctxt' = fold Variable.auto_fixes lhss' lthy;
in Variable.export_terms ctxt' lthy lhss' end
|> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
proc = proc,
--- a/src/Pure/thm.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Pure/thm.ML Fri Nov 04 13:52:19 2011 +0100
@@ -1494,7 +1494,7 @@
if short < 0 then error "More names than abstractions!"
else Name.variant_list cs (take short iparams) @ cs;
val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
- val newBi = Logic.list_rename_params (newnames, Bi);
+ val newBi = Logic.list_rename_params newnames Bi;
in
(case duplicates (op =) cs of
a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state)
--- a/src/Tools/induct.ML Fri Nov 04 08:19:24 2011 +0100
+++ b/src/Tools/induct.ML Fri Nov 04 13:52:19 2011 +0100
@@ -627,7 +627,7 @@
val xs' =
(case filter (fn x' => x' = x) xs of
[] => xs | [_] => xs | _ => index 1 xs);
- in Logic.list_rename_params (xs', A) end;
+ in Logic.list_rename_params xs' A end;
fun rename_prop p =
let val (As, C) = Logic.strip_horn p
in Logic.list_implies (map rename_asm As, C) end;