--- a/src/Pure/Isar/auto_bind.ML Mon Nov 02 20:38:46 2009 +0100
+++ b/src/Pure/Isar/auto_bind.ML Mon Nov 02 20:45:23 2009 +0100
@@ -14,7 +14,7 @@
val no_facts: (indexname * term option) list
end;
-structure AutoBind: AUTO_BIND =
+structure Auto_Bind: AUTO_BIND =
struct
(** bindings **)
--- a/src/Pure/Isar/obtain.ML Mon Nov 02 20:38:46 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Nov 02 20:45:23 2009 +0100
@@ -129,7 +129,7 @@
val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
(*obtain statements*)
- val thesisN = Name.variant xs AutoBind.thesisN;
+ val thesisN = Name.variant xs Auto_Bind.thesisN;
val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
val asm_frees = fold Term.add_frees asm_props [];
@@ -142,7 +142,7 @@
Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
|> Library.curry Logic.list_rename_params xs;
val obtain_prop =
- Logic.list_rename_params ([AutoBind.thesisN],
+ Logic.list_rename_params ([Auto_Bind.thesisN],
Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
fun after_qed _ =
@@ -189,7 +189,7 @@
val thy = ProofContext.theory_of ctxt;
val cert = Thm.cterm_of thy;
- val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt AutoBind.thesisN;
+ val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
val rule =
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
@@ -273,7 +273,7 @@
val ctxt = Proof.context_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
- val (thesis_var, thesis) = #1 (bind_judgment ctxt AutoBind.thesisN);
+ val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
fun guess_context raw_rule state' =
@@ -293,7 +293,7 @@
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
- |> Proof.bind_terms AutoBind.no_facts
+ |> Proof.bind_terms Auto_Bind.no_facts
end;
val goal = Var (("guess", 0), propT);
@@ -307,7 +307,7 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
+ |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
--- a/src/Pure/Isar/proof.ML Mon Nov 02 20:38:46 2009 +0100
+++ b/src/Pure/Isar/proof.ML Mon Nov 02 20:45:23 2009 +0100
@@ -225,7 +225,7 @@
fun put_facts facts =
map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
- put_thms true (AutoBind.thisN, facts);
+ put_thms true (Auto_Bind.thisN, facts);
fun these_factss more_facts (named_factss, state) =
(named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
@@ -710,7 +710,7 @@
in
state'
|> assume_i assumptions
- |> bind_terms AutoBind.no_facts
+ |> bind_terms Auto_Bind.no_facts
|> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
@@ -1026,10 +1026,10 @@
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
- fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
- fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+ fun after_local' [[th]] = put_thms false (Auto_Bind.thisN, SOME [th]);
+ fun after_global' [[th]] = ProofContext.put_thms false (Auto_Bind.thisN, SOME [th]);
val after_qed' = (after_local', after_global');
- val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN);
+ val this_name = ProofContext.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
val result_ctxt =
state
--- a/src/Pure/Isar/proof_context.ML Mon Nov 02 20:38:46 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Nov 02 20:45:23 2009 +0100
@@ -773,8 +773,8 @@
fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
-val auto_bind_goal = auto_bind AutoBind.goal;
-val auto_bind_facts = auto_bind AutoBind.facts;
+val auto_bind_goal = auto_bind Auto_Bind.goal;
+val auto_bind_facts = auto_bind Auto_Bind.facts;
(* match_bind(_i) *)
--- a/src/Pure/Isar/specification.ML Mon Nov 02 20:38:46 2009 +0100
+++ b/src/Pure/Isar/specification.ML Mon Nov 02 20:45:23 2009 +0100
@@ -298,7 +298,7 @@
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
- val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
+ val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
@@ -323,7 +323,7 @@
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths => ProofContext.note_thmss Thm.assumptionK
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
@@ -369,7 +369,7 @@
in
goal_ctxt
|> ProofContext.note_thmss Thm.assumptionK
- [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
+ [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)