# HG changeset patch
# User wenzelm
# Date 1272203523 -7200
# Node ID 655e2d74de3af5a36db9405d60f59409c308aa5d
# Parent  81cba3921ba51ce2c1e83c5fedec8cdf2d3cf22a
modernized naming conventions of main Isar proof elements;

diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -99,7 +99,7 @@
     |> (fn ctxt1 => ctxt1
     |> prepare
     |-> (fn us => fn ctxt2 => ctxt2
-    |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+    |> Proof.theorem NONE (fn thmss => fn ctxt =>
          let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
          in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
   end
@@ -188,7 +188,7 @@
 
   fun prove thy meth vc =
     ProofContext.init thy
-    |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
+    |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
     |> Proof.apply meth
     |> Seq.hd
     |> Proof.global_done_proof
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -543,7 +543,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem_i NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -445,7 +445,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem_i NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -363,7 +363,7 @@
   in
     lthy' |>
     Variable.add_fixes (map fst lsrs) |> snd |>
-    Proof.theorem_i NONE
+    Proof.theorem NONE
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -436,7 +436,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+    |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -120,7 +120,7 @@
       end
   in
     lthy
-    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   end
 
@@ -177,7 +177,7 @@
     |> ProofContext.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
          [([Goal.norm_result termination], [])])] |> snd
-    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+    |> Proof.theorem NONE afterqed [[(goal, [])]]
   end
 
 val termination_proof = gen_termination_proof Syntax.check_term
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -3059,7 +3059,7 @@
            ) options [const]))
       end
   in
-    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
+    Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;
 
 val code_pred = generic_code_pred (K I);
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -45,7 +45,7 @@
   val goals' = map (rpair []) goals
   fun after_qed' thms = after_qed (the_single thms)
 in
-  Proof.theorem_i NONE after_qed' [goals'] ctxt
+  Proof.theorem NONE after_qed' [goals'] ctxt
 end
 
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -226,7 +226,7 @@
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+      |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;
 
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -282,7 +282,7 @@
     val ((goal, goal_pat, typedef_result), lthy') =
       prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
     fun after_qed [[th]] = snd o typedef_result th;
-  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
+  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
 
 in
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -328,7 +328,7 @@
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 fun gen_pcpodef_proof prep_term prep_constraint
     ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
@@ -339,7 +339,7 @@
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 in
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/calculation.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -13,11 +13,11 @@
   val sym_add: attribute
   val sym_del: attribute
   val symmetric: attribute
-  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
+  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
-  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state
 end;
@@ -148,10 +148,10 @@
         state |> maintain_calculation final calc))
   end;
 
-val also = calculate Proof.get_thmss false;
-val also_i = calculate (K I) false;
-val finally = calculate Proof.get_thmss true;
-val finally_i = calculate (K I) true;
+val also = calculate (K I) false;
+val also_cmd = calculate Proof.get_thmss_cmd false;
+val finally = calculate (K I) true;
+val finally_cmd = calculate Proof.get_thmss_cmd true;
 
 
 (* moreover and ultimately *)
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -370,7 +370,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   end;
 
 in
@@ -539,7 +539,7 @@
   end;
 
 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
-  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
+  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
 
 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
@@ -595,7 +595,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/element.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -283,10 +283,10 @@
 in
 
 fun witness_proof after_qed wit_propss =
-  gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+  gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
     wit_propss [];
 
-val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
 
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   gen_witness_proof (fn after_qed' => fn propss =>
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -219,10 +219,10 @@
 fun goal opt_chain goal stmt int =
   opt_chain #> goal NONE (K I) stmt int;
 
-val have = goal I Proof.have;
-val hence = goal Proof.chain Proof.have;
-val show = goal I Proof.show;
-val thus = goal Proof.chain Proof.show;
+val have = goal I Proof.have_cmd;
+val hence = goal Proof.chain Proof.have_cmd;
+val show = goal I Proof.show_cmd;
+val thus = goal Proof.chain Proof.show_cmd;
 
 
 (* local endings *)
@@ -403,7 +403,7 @@
   in Present.display_graph gr end);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
 
 
 (* find unused theorems *)
@@ -437,12 +437,12 @@
 local
 
 fun string_of_stmts state args =
-  Proof.get_thmss state args
+  Proof.get_thmss_cmd state args
   |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
   |> Pretty.chunks2 |> Pretty.string_of;
 
 fun string_of_thms state args =
-  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
+  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
@@ -460,7 +460,7 @@
         end
     | SOME args => Pretty.chunks
         (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
-          (Proof.get_thmss state args)));
+          (Proof.get_thmss_cmd state args)));
 
 fun string_of_prop state s =
   let
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -542,27 +542,27 @@
 val _ =
   OuterSyntax.command "from" "forward chaining from given facts"
     (K.tag_proof K.prf_chain)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "with" "forward chaining from given and current facts"
     (K.tag_proof K.prf_chain)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "note" "define facts"
     (K.tag_proof K.prf_decl)
-    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
+    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "using" "augment goal facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
 
 val _ =
   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
 
 
 (* proof context *)
@@ -570,17 +570,17 @@
 val _ =
   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
     (K.tag_proof K.prf_asm)
-    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
 
 val _ =
   OuterSyntax.command "assume" "assume propositions"
     (K.tag_proof K.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
+    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
 
 val _ =
   OuterSyntax.command "presume" "assume propositions, to be established later"
     (K.tag_proof K.prf_asm)
-    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
+    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
 
 val _ =
   OuterSyntax.command "def" "local definition"
@@ -588,24 +588,24 @@
     (P.and_list1
       (SpecParse.opt_thm_name ":" --
         ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
-    >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
+    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
   OuterSyntax.command "obtain" "generalized existence"
     (K.tag_proof K.prf_asm_goal)
     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
-      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
+      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
   OuterSyntax.command "guess" "wild guessing (unstructured)"
     (K.tag_proof K.prf_asm_goal)
-    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
 
 val _ =
   OuterSyntax.command "let" "bind text variables"
     (K.tag_proof K.prf_decl)
     (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
-      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
+      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
 val case_spec =
   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
@@ -614,7 +614,7 @@
 val _ =
   OuterSyntax.command "case" "invoke local context"
     (K.tag_proof K.prf_asm)
-    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
+    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
 
 
 (* proof structure *)
@@ -711,12 +711,12 @@
 val _ =
   OuterSyntax.command "also" "combine calculation and current facts"
     (K.tag_proof K.prf_decl)
-    (calc_args >> (Toplevel.proofs' o Calculation.also));
+    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     (K.tag_proof K.prf_chain)
-    (calc_args >> (Toplevel.proofs' o Calculation.finally));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -39,14 +39,14 @@
 signature OBTAIN =
 sig
   val thatN: string
-  val obtain: string -> (binding * string option * mixfix) list ->
+  val obtain: string -> (binding * typ option * mixfix) list ->
+    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
+  val obtain_cmd: string -> (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val obtain_i: string -> (binding * typ option * mixfix) list ->
-    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     ((string * cterm) list * thm list) * Proof.context
-  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
-  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;
 
 structure Obtain: OBTAIN =
@@ -148,26 +148,26 @@
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> `Proof.the_fact #-> (fn rule =>
-        Proof.fix_i vars
-        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
+        Proof.fix vars
+        #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
-    |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
-    |> Proof.assume_i
+    |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
+    |> Proof.assume
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
 in
 
-val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
-val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
 
 end;
 
@@ -290,8 +290,8 @@
       in
         state'
         |> Proof.map_context (K ctxt')
-        |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
-        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
+        |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
+        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
         |> Proof.bind_terms Auto_Bind.no_facts
       end;
@@ -307,7 +307,7 @@
     state
     |> Proof.enter_forward
     |> Proof.begin_block
-    |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+    |> Proof.fix [(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])]
@@ -316,8 +316,8 @@
 
 in
 
-val guess = gen_guess ProofContext.read_vars;
-val guess_i = gen_guess ProofContext.cert_vars;
+val guess = gen_guess ProofContext.cert_vars;
+val guess_cmd = gen_guess ProofContext.read_vars;
 
 end;
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -41,37 +41,37 @@
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
-  val match_bind: (string list * string) list -> state -> state
-  val match_bind_i: (term list * term) list -> state -> state
-  val let_bind: (string list * string) list -> state -> state
-  val let_bind_i: (term list * term) list -> state -> state
-  val fix: (binding * string option * mixfix) list -> state -> state
-  val fix_i: (binding * typ option * mixfix) list -> state -> state
+  val match_bind: (term list * term) list -> state -> state
+  val match_bind_cmd: (string list * string) list -> state -> state
+  val let_bind: (term list * term) list -> state -> state
+  val let_bind_cmd: (string list * string) list -> state -> state
+  val fix: (binding * typ option * mixfix) list -> state -> state
+  val fix_cmd: (binding * string option * mixfix) list -> state -> state
   val assm: Assumption.export ->
+    (Thm.binding * (term * term list) list) list -> state -> state
+  val assm_cmd: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
-  val assm_i: Assumption.export ->
-    (Thm.binding * (term * term list) list) list -> state -> state
-  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
-  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
-  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
-  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+  val assume: (Thm.binding * (term * term list) list) list -> state -> state
+  val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+  val presume: (Thm.binding * (term * term list) list) list -> state -> state
+  val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
-  val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
-  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
-  val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
-  val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val using_i: ((thm list * attribute list) list) list -> state -> state
-  val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val unfolding_i: ((thm list * attribute list) list) list -> state -> state
-  val invoke_case: string * string option list * Attrib.src list -> state -> state
-  val invoke_case_i: string * string option list * attribute list -> state -> state
+  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
+  val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+  val from_thmss: ((thm list * attribute list) list) list -> state -> state
+  val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val with_thmss: ((thm list * attribute list) list) list -> state -> state
+  val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val using: ((thm list * attribute list) list) list -> state -> state
+  val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val unfolding: ((thm list * attribute list) list) list -> state -> state
+  val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val invoke_case: string * string option list * attribute list -> state -> state
+  val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
@@ -87,9 +87,9 @@
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
+    (term * term list) list list -> context -> state
+  val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
-  val theorem_i: Method.text option -> (thm list list -> context -> context) ->
-    (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
   val local_terminal_proof: Method.text * Method.text option -> state -> state
   val local_default_proof: state -> state
@@ -102,13 +102,13 @@
   val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
   val have: Method.text option -> (thm list list -> state -> state) ->
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+  val have_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val have_i: Method.text option -> (thm list list -> state -> state) ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+  val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val show_i: Method.text option -> (thm list list -> state -> state) ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
@@ -535,10 +535,10 @@
 
 in
 
-val match_bind = gen_bind (ProofContext.match_bind false);
-val match_bind_i = gen_bind (ProofContext.match_bind_i false);
-val let_bind = gen_bind (ProofContext.match_bind true);
-val let_bind_i = gen_bind (ProofContext.match_bind_i true);
+val match_bind = gen_bind (ProofContext.match_bind_i false);
+val match_bind_cmd = gen_bind (ProofContext.match_bind false);
+val let_bind = gen_bind (ProofContext.match_bind_i true);
+val let_bind_cmd = gen_bind (ProofContext.match_bind true);
 
 end;
 
@@ -554,8 +554,8 @@
 
 in
 
-val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
-val fix_i = gen_fix (K I);
+val fix = gen_fix (K I);
+val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
 
 end;
 
@@ -572,12 +572,12 @@
 
 in
 
-val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
-val assm_i    = gen_assume ProofContext.add_assms_i (K I);
-val assume    = assm Assumption.assume_export;
-val assume_i  = assm_i Assumption.assume_export;
-val presume   = assm Assumption.presume_export;
-val presume_i = assm_i Assumption.presume_export;
+val assm = gen_assume ProofContext.add_assms_i (K I);
+val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
+val assume = assm Assumption.assume_export;
+val assume_cmd = assm_cmd Assumption.assume_export;
+val presume = assm Assumption.presume_export;
+val presume_cmd = assm_cmd Assumption.presume_export;
 
 end;
 
@@ -605,8 +605,8 @@
 
 in
 
-val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
-val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
 
 end;
 
@@ -646,18 +646,18 @@
 
 in
 
-val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
 
-val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
 
-val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
-fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
+fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
 
 end;
 
@@ -686,10 +686,10 @@
 
 in
 
-val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
-val using_i = gen_using append_using (K (K I)) (K I) (K I);
-val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
-val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
+val using = gen_using append_using (K (K I)) (K I) (K I);
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
 
 end;
 
@@ -709,15 +709,15 @@
     val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'
-    |> assume_i assumptions
+    |> assume assumptions
     |> bind_terms Auto_Bind.no_facts
-    |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
+    |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
   end;
 
 in
 
-val invoke_case = gen_invoke_case Attrib.attribute;
-val invoke_case_i = gen_invoke_case (K I);
+val invoke_case = gen_invoke_case (K I);
+val invoke_case_cmd = gen_invoke_case Attrib.attribute;
 
 end;
 
@@ -901,8 +901,8 @@
   init ctxt
   |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
 
-val theorem = global_goal ProofContext.bind_propp_schematic;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
+val theorem = global_goal ProofContext.bind_propp_schematic_i;
+val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
 
 fun global_qeds txt =
   end_proof true txt
@@ -974,10 +974,10 @@
 
 in
 
-val have = gen_have Attrib.attribute ProofContext.bind_propp;
-val have_i = gen_have (K I) ProofContext.bind_propp_i;
-val show = gen_show Attrib.attribute ProofContext.bind_propp;
-val show_i = gen_show (K I) ProofContext.bind_propp_i;
+val have = gen_have (K I) ProofContext.bind_propp_i;
+val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
+val show = gen_show (K I) ProofContext.bind_propp_i;
+val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
 
 end;
 
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -403,7 +403,7 @@
     goal_ctxt
     |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
     |> snd
-    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+    |> Proof.theorem before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
         error "Illegal schematic goal statement")
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -64,7 +64,7 @@
         fun after_qed res goal_ctxt =
           put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
         val ctxt' = ctxt
-          |> Proof.theorem_i NONE after_qed propss
+          |> Proof.theorem NONE after_qed propss
           |> Proof.global_terminal_proof methods;
         val (a, background') = background
           |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
diff -r 81cba3921ba5 -r 655e2d74de3a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -574,7 +574,7 @@
       val prop_src =
         (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
       val _ = context
-        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+        |> Proof.theorem NONE (K I) [[(prop, [])]]
         |> Proof.global_terminal_proof methods;
     in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);