# HG changeset patch # User wenzelm # Date 1257191123 -3600 # Node ID ff29d1549acad7113d3460358b7c98deda823ed3 # Parent fb2358edcfb6a8ec137614ac9283dc575a0d310b modernized structure AutoBind; diff -r fb2358edcfb6 -r ff29d1549aca src/Pure/Isar/auto_bind.ML --- 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 **) diff -r fb2358edcfb6 -r ff29d1549aca src/Pure/Isar/obtain.ML --- 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])] diff -r fb2358edcfb6 -r ff29d1549aca src/Pure/Isar/proof.ML --- 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 diff -r fb2358edcfb6 -r ff29d1549aca src/Pure/Isar/proof_context.ML --- 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) *) diff -r fb2358edcfb6 -r ff29d1549aca src/Pure/Isar/specification.ML --- 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)