modernized naming conventions of main Isar proof elements;
authorwenzelm
Sun Apr 25 15:52:03 2010 +0200 (2010-04-25)
changeset 36323655e2d74de3a
parent 36322 81cba3921ba5
child 36324 7cd5057a5bb8
modernized naming conventions of main Isar proof elements;
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/typedef.ML
src/HOLCF/Tools/pcpodef.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_thms.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 15:13:33 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Apr 25 15:52:03 2010 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4      |> (fn ctxt1 => ctxt1
     1.5      |> prepare
     1.6      |-> (fn us => fn ctxt2 => ctxt2
     1.7 -    |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
     1.8 +    |> Proof.theorem NONE (fn thmss => fn ctxt =>
     1.9           let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
    1.10           in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
    1.11    end
    1.12 @@ -188,7 +188,7 @@
    1.13  
    1.14    fun prove thy meth vc =
    1.15      ProofContext.init thy
    1.16 -    |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
    1.17 +    |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
    1.18      |> Proof.apply meth
    1.19      |> Seq.hd
    1.20      |> Proof.global_done_proof
     2.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:13:33 2010 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:52:03 2010 +0200
     2.3 @@ -543,7 +543,7 @@
     2.4  
     2.5    in
     2.6      ctxt'' |>
     2.7 -    Proof.theorem_i NONE (fn thss => fn ctxt =>
     2.8 +    Proof.theorem NONE (fn thss => fn ctxt =>
     2.9        let
    2.10          val rec_name = space_implode "_" (map Long_Name.base_name names);
    2.11          val rec_qualified = Binding.qualify false rec_name;
     3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:13:33 2010 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:52:03 2010 +0200
     3.3 @@ -445,7 +445,7 @@
     3.4  
     3.5    in
     3.6      ctxt'' |>
     3.7 -    Proof.theorem_i NONE (fn thss => fn ctxt =>
     3.8 +    Proof.theorem NONE (fn thss => fn ctxt =>
     3.9        let
    3.10          val rec_name = space_implode "_" (map Long_Name.base_name names);
    3.11          val rec_qualified = Binding.qualify false rec_name;
     4.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:13:33 2010 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:52:03 2010 +0200
     4.3 @@ -363,7 +363,7 @@
     4.4    in
     4.5      lthy' |>
     4.6      Variable.add_fixes (map fst lsrs) |> snd |>
     4.7 -    Proof.theorem_i NONE
     4.8 +    Proof.theorem NONE
     4.9        (fn thss => fn goal_ctxt =>
    4.10           let
    4.11             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
     5.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:13:33 2010 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Apr 25 15:52:03 2010 +0200
     5.3 @@ -436,7 +436,7 @@
     5.4    in
     5.5      thy
     5.6      |> ProofContext.init
     5.7 -    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
     5.8 +    |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
     5.9    end;
    5.10  
    5.11  val rep_datatype = gen_rep_datatype Sign.cert_term;
     6.1 --- a/src/HOL/Tools/Function/function.ML	Sun Apr 25 15:13:33 2010 +0200
     6.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Apr 25 15:52:03 2010 +0200
     6.3 @@ -120,7 +120,7 @@
     6.4        end
     6.5    in
     6.6      lthy
     6.7 -    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     6.8 +    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     6.9      |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    6.10    end
    6.11  
    6.12 @@ -177,7 +177,7 @@
    6.13      |> ProofContext.note_thmss ""
    6.14         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
    6.15           [([Goal.norm_result termination], [])])] |> snd
    6.16 -    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
    6.17 +    |> Proof.theorem NONE afterqed [[(goal, [])]]
    6.18    end
    6.19  
    6.20  val termination_proof = gen_termination_proof Syntax.check_term
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:13:33 2010 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:52:03 2010 +0200
     7.3 @@ -3059,7 +3059,7 @@
     7.4             ) options [const]))
     7.5        end
     7.6    in
     7.7 -    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
     7.8 +    Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
     7.9    end;
    7.10  
    7.11  val code_pred = generic_code_pred (K I);
     8.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:13:33 2010 +0200
     8.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:52:03 2010 +0200
     8.3 @@ -45,7 +45,7 @@
     8.4    val goals' = map (rpair []) goals
     8.5    fun after_qed' thms = after_qed (the_single thms)
     8.6  in
     8.7 -  Proof.theorem_i NONE after_qed' [goals'] ctxt
     8.8 +  Proof.theorem NONE after_qed' [goals'] ctxt
     8.9  end
    8.10  
    8.11  
     9.1 --- a/src/HOL/Tools/choice_specification.ML	Sun Apr 25 15:13:33 2010 +0200
     9.2 +++ b/src/HOL/Tools/choice_specification.ML	Sun Apr 25 15:52:03 2010 +0200
     9.3 @@ -226,7 +226,7 @@
     9.4      in
     9.5        thy
     9.6        |> ProofContext.init
     9.7 -      |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     9.8 +      |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     9.9      end;
    9.10  
    9.11  
    10.1 --- a/src/HOL/Tools/typedef.ML	Sun Apr 25 15:13:33 2010 +0200
    10.2 +++ b/src/HOL/Tools/typedef.ML	Sun Apr 25 15:52:03 2010 +0200
    10.3 @@ -282,7 +282,7 @@
    10.4      val ((goal, goal_pat, typedef_result), lthy') =
    10.5        prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
    10.6      fun after_qed [[th]] = snd o typedef_result th;
    10.7 -  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
    10.8 +  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
    10.9  
   10.10  in
   10.11  
    11.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 15:13:33 2010 +0200
    11.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sun Apr 25 15:52:03 2010 +0200
    11.3 @@ -328,7 +328,7 @@
    11.4        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
    11.5      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
    11.6        | after_qed _ = raise Fail "cpodef_proof";
    11.7 -  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    11.8 +  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    11.9  
   11.10  fun gen_pcpodef_proof prep_term prep_constraint
   11.11      ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   11.12 @@ -339,7 +339,7 @@
   11.13        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
   11.14      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
   11.15        | after_qed _ = raise Fail "pcpodef_proof";
   11.16 -  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   11.17 +  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   11.18  
   11.19  in
   11.20  
    12.1 --- a/src/Pure/Isar/calculation.ML	Sun Apr 25 15:13:33 2010 +0200
    12.2 +++ b/src/Pure/Isar/calculation.ML	Sun Apr 25 15:52:03 2010 +0200
    12.3 @@ -13,11 +13,11 @@
    12.4    val sym_add: attribute
    12.5    val sym_del: attribute
    12.6    val symmetric: attribute
    12.7 -  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    12.8 -  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    12.9 -  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
   12.10 +  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   12.11 +  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   12.12 +  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   12.13 +  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
   12.14      Proof.state -> Proof.state Seq.seq
   12.15 -  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   12.16    val moreover: bool -> Proof.state -> Proof.state
   12.17    val ultimately: bool -> Proof.state -> Proof.state
   12.18  end;
   12.19 @@ -148,10 +148,10 @@
   12.20          state |> maintain_calculation final calc))
   12.21    end;
   12.22  
   12.23 -val also = calculate Proof.get_thmss false;
   12.24 -val also_i = calculate (K I) false;
   12.25 -val finally = calculate Proof.get_thmss true;
   12.26 -val finally_i = calculate (K I) true;
   12.27 +val also = calculate (K I) false;
   12.28 +val also_cmd = calculate Proof.get_thmss_cmd false;
   12.29 +val finally = calculate (K I) true;
   12.30 +val finally_cmd = calculate Proof.get_thmss_cmd true;
   12.31  
   12.32  
   12.33  (* moreover and ultimately *)
    13.1 --- a/src/Pure/Isar/class_target.ML	Sun Apr 25 15:13:33 2010 +0200
    13.2 +++ b/src/Pure/Isar/class_target.ML	Sun Apr 25 15:52:03 2010 +0200
    13.3 @@ -370,7 +370,7 @@
    13.4    in
    13.5      thy
    13.6      |> ProofContext.init
    13.7 -    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
    13.8 +    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
    13.9    end;
   13.10  
   13.11  in
   13.12 @@ -539,7 +539,7 @@
   13.13    end;
   13.14  
   13.15  val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   13.16 -  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   13.17 +  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   13.18  
   13.19  fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   13.20    fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   13.21 @@ -595,7 +595,7 @@
   13.22    in
   13.23      thy
   13.24      |> ProofContext.init
   13.25 -    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
   13.26 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   13.27    end;
   13.28  
   13.29  
    14.1 --- a/src/Pure/Isar/element.ML	Sun Apr 25 15:13:33 2010 +0200
    14.2 +++ b/src/Pure/Isar/element.ML	Sun Apr 25 15:52:03 2010 +0200
    14.3 @@ -283,10 +283,10 @@
    14.4  in
    14.5  
    14.6  fun witness_proof after_qed wit_propss =
    14.7 -  gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
    14.8 +  gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
    14.9      wit_propss [];
   14.10  
   14.11 -val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
   14.12 +val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
   14.13  
   14.14  fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   14.15    gen_witness_proof (fn after_qed' => fn propss =>
    15.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:13:33 2010 +0200
    15.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:52:03 2010 +0200
    15.3 @@ -219,10 +219,10 @@
    15.4  fun goal opt_chain goal stmt int =
    15.5    opt_chain #> goal NONE (K I) stmt int;
    15.6  
    15.7 -val have = goal I Proof.have;
    15.8 -val hence = goal Proof.chain Proof.have;
    15.9 -val show = goal I Proof.show;
   15.10 -val thus = goal Proof.chain Proof.show;
   15.11 +val have = goal I Proof.have_cmd;
   15.12 +val hence = goal Proof.chain Proof.have_cmd;
   15.13 +val show = goal I Proof.show_cmd;
   15.14 +val thus = goal Proof.chain Proof.show_cmd;
   15.15  
   15.16  
   15.17  (* local endings *)
   15.18 @@ -403,7 +403,7 @@
   15.19    in Present.display_graph gr end);
   15.20  
   15.21  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   15.22 -  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
   15.23 +  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
   15.24  
   15.25  
   15.26  (* find unused theorems *)
   15.27 @@ -437,12 +437,12 @@
   15.28  local
   15.29  
   15.30  fun string_of_stmts state args =
   15.31 -  Proof.get_thmss state args
   15.32 +  Proof.get_thmss_cmd state args
   15.33    |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
   15.34    |> Pretty.chunks2 |> Pretty.string_of;
   15.35  
   15.36  fun string_of_thms state args =
   15.37 -  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
   15.38 +  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
   15.39  
   15.40  fun string_of_prfs full state arg =
   15.41    Pretty.string_of
   15.42 @@ -460,7 +460,7 @@
   15.43          end
   15.44      | SOME args => Pretty.chunks
   15.45          (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
   15.46 -          (Proof.get_thmss state args)));
   15.47 +          (Proof.get_thmss_cmd state args)));
   15.48  
   15.49  fun string_of_prop state s =
   15.50    let
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 25 15:13:33 2010 +0200
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 25 15:52:03 2010 +0200
    16.3 @@ -542,27 +542,27 @@
    16.4  val _ =
    16.5    OuterSyntax.command "from" "forward chaining from given facts"
    16.6      (K.tag_proof K.prf_chain)
    16.7 -    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
    16.8 +    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
    16.9  
   16.10  val _ =
   16.11    OuterSyntax.command "with" "forward chaining from given and current facts"
   16.12      (K.tag_proof K.prf_chain)
   16.13 -    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
   16.14 +    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
   16.15  
   16.16  val _ =
   16.17    OuterSyntax.command "note" "define facts"
   16.18      (K.tag_proof K.prf_decl)
   16.19 -    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   16.20 +    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
   16.21  
   16.22  val _ =
   16.23    OuterSyntax.command "using" "augment goal facts"
   16.24      (K.tag_proof K.prf_decl)
   16.25 -    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
   16.26 +    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
   16.27  
   16.28  val _ =
   16.29    OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   16.30      (K.tag_proof K.prf_decl)
   16.31 -    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
   16.32 +    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
   16.33  
   16.34  
   16.35  (* proof context *)
   16.36 @@ -570,17 +570,17 @@
   16.37  val _ =
   16.38    OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   16.39      (K.tag_proof K.prf_asm)
   16.40 -    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
   16.41 +    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
   16.42  
   16.43  val _ =
   16.44    OuterSyntax.command "assume" "assume propositions"
   16.45      (K.tag_proof K.prf_asm)
   16.46 -    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   16.47 +    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
   16.48  
   16.49  val _ =
   16.50    OuterSyntax.command "presume" "assume propositions, to be established later"
   16.51      (K.tag_proof K.prf_asm)
   16.52 -    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   16.53 +    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
   16.54  
   16.55  val _ =
   16.56    OuterSyntax.command "def" "local definition"
   16.57 @@ -588,24 +588,24 @@
   16.58      (P.and_list1
   16.59        (SpecParse.opt_thm_name ":" --
   16.60          ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   16.61 -    >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   16.62 +    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
   16.63  
   16.64  val _ =
   16.65    OuterSyntax.command "obtain" "generalized existence"
   16.66      (K.tag_proof K.prf_asm_goal)
   16.67      (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   16.68 -      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   16.69 +      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
   16.70  
   16.71  val _ =
   16.72    OuterSyntax.command "guess" "wild guessing (unstructured)"
   16.73      (K.tag_proof K.prf_asm_goal)
   16.74 -    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
   16.75 +    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
   16.76  
   16.77  val _ =
   16.78    OuterSyntax.command "let" "bind text variables"
   16.79      (K.tag_proof K.prf_decl)
   16.80      (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
   16.81 -      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
   16.82 +      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
   16.83  
   16.84  val case_spec =
   16.85    (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   16.86 @@ -614,7 +614,7 @@
   16.87  val _ =
   16.88    OuterSyntax.command "case" "invoke local context"
   16.89      (K.tag_proof K.prf_asm)
   16.90 -    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
   16.91 +    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
   16.92  
   16.93  
   16.94  (* proof structure *)
   16.95 @@ -711,12 +711,12 @@
   16.96  val _ =
   16.97    OuterSyntax.command "also" "combine calculation and current facts"
   16.98      (K.tag_proof K.prf_decl)
   16.99 -    (calc_args >> (Toplevel.proofs' o Calculation.also));
  16.100 +    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
  16.101  
  16.102  val _ =
  16.103    OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
  16.104      (K.tag_proof K.prf_chain)
  16.105 -    (calc_args >> (Toplevel.proofs' o Calculation.finally));
  16.106 +    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
  16.107  
  16.108  val _ =
  16.109    OuterSyntax.command "moreover" "augment calculation by current facts"
    17.1 --- a/src/Pure/Isar/obtain.ML	Sun Apr 25 15:13:33 2010 +0200
    17.2 +++ b/src/Pure/Isar/obtain.ML	Sun Apr 25 15:52:03 2010 +0200
    17.3 @@ -39,14 +39,14 @@
    17.4  signature OBTAIN =
    17.5  sig
    17.6    val thatN: string
    17.7 -  val obtain: string -> (binding * string option * mixfix) list ->
    17.8 +  val obtain: string -> (binding * typ option * mixfix) list ->
    17.9 +    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   17.10 +  val obtain_cmd: string -> (binding * string option * mixfix) list ->
   17.11      (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   17.12 -  val obtain_i: string -> (binding * typ option * mixfix) list ->
   17.13 -    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   17.14    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
   17.15      ((string * cterm) list * thm list) * Proof.context
   17.16 -  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   17.17 -  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   17.18 +  val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   17.19 +  val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   17.20  end;
   17.21  
   17.22  structure Obtain: OBTAIN =
   17.23 @@ -148,26 +148,26 @@
   17.24      fun after_qed _ =
   17.25        Proof.local_qed (NONE, false)
   17.26        #> `Proof.the_fact #-> (fn rule =>
   17.27 -        Proof.fix_i vars
   17.28 -        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   17.29 +        Proof.fix vars
   17.30 +        #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   17.31    in
   17.32      state
   17.33      |> Proof.enter_forward
   17.34 -    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
   17.35 +    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
   17.36      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   17.37 -    |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
   17.38 -    |> Proof.assume_i
   17.39 +    |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
   17.40 +    |> Proof.assume
   17.41        [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
   17.42      |> `Proof.the_facts
   17.43      ||> Proof.chain_facts chain_facts
   17.44 -    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
   17.45 +    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
   17.46      |-> Proof.refine_insert
   17.47    end;
   17.48  
   17.49  in
   17.50  
   17.51 -val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
   17.52 -val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   17.53 +val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   17.54 +val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
   17.55  
   17.56  end;
   17.57  
   17.58 @@ -290,8 +290,8 @@
   17.59        in
   17.60          state'
   17.61          |> Proof.map_context (K ctxt')
   17.62 -        |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
   17.63 -        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
   17.64 +        |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
   17.65 +        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
   17.66            (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
   17.67          |> Proof.bind_terms Auto_Bind.no_facts
   17.68        end;
   17.69 @@ -307,7 +307,7 @@
   17.70      state
   17.71      |> Proof.enter_forward
   17.72      |> Proof.begin_block
   17.73 -    |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
   17.74 +    |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
   17.75      |> Proof.chain_facts chain_facts
   17.76      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
   17.77        "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
   17.78 @@ -316,8 +316,8 @@
   17.79  
   17.80  in
   17.81  
   17.82 -val guess = gen_guess ProofContext.read_vars;
   17.83 -val guess_i = gen_guess ProofContext.cert_vars;
   17.84 +val guess = gen_guess ProofContext.cert_vars;
   17.85 +val guess_cmd = gen_guess ProofContext.read_vars;
   17.86  
   17.87  end;
   17.88  
    18.1 --- a/src/Pure/Isar/proof.ML	Sun Apr 25 15:13:33 2010 +0200
    18.2 +++ b/src/Pure/Isar/proof.ML	Sun Apr 25 15:52:03 2010 +0200
    18.3 @@ -41,37 +41,37 @@
    18.4    val raw_goal: state -> {context: context, facts: thm list, goal: thm}
    18.5    val goal: state -> {context: context, facts: thm list, goal: thm}
    18.6    val simple_goal: state -> {context: context, goal: thm}
    18.7 -  val match_bind: (string list * string) list -> state -> state
    18.8 -  val match_bind_i: (term list * term) list -> state -> state
    18.9 -  val let_bind: (string list * string) list -> state -> state
   18.10 -  val let_bind_i: (term list * term) list -> state -> state
   18.11 -  val fix: (binding * string option * mixfix) list -> state -> state
   18.12 -  val fix_i: (binding * typ option * mixfix) list -> state -> state
   18.13 +  val match_bind: (term list * term) list -> state -> state
   18.14 +  val match_bind_cmd: (string list * string) list -> state -> state
   18.15 +  val let_bind: (term list * term) list -> state -> state
   18.16 +  val let_bind_cmd: (string list * string) list -> state -> state
   18.17 +  val fix: (binding * typ option * mixfix) list -> state -> state
   18.18 +  val fix_cmd: (binding * string option * mixfix) list -> state -> state
   18.19    val assm: Assumption.export ->
   18.20 +    (Thm.binding * (term * term list) list) list -> state -> state
   18.21 +  val assm_cmd: Assumption.export ->
   18.22      (Attrib.binding * (string * string list) list) list -> state -> state
   18.23 -  val assm_i: Assumption.export ->
   18.24 -    (Thm.binding * (term * term list) list) list -> state -> state
   18.25 -  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   18.26 -  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
   18.27 -  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   18.28 -  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
   18.29 -  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   18.30 -  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   18.31 +  val assume: (Thm.binding * (term * term list) list) list -> state -> state
   18.32 +  val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
   18.33 +  val presume: (Thm.binding * (term * term list) list) list -> state -> state
   18.34 +  val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
   18.35 +  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   18.36 +  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   18.37    val chain: state -> state
   18.38    val chain_facts: thm list -> state -> state
   18.39 -  val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   18.40 -  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   18.41 -  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   18.42 -  val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.43 -  val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   18.44 -  val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.45 -  val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
   18.46 -  val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.47 -  val using_i: ((thm list * attribute list) list) list -> state -> state
   18.48 -  val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.49 -  val unfolding_i: ((thm list * attribute list) list) list -> state -> state
   18.50 -  val invoke_case: string * string option list * Attrib.src list -> state -> state
   18.51 -  val invoke_case_i: string * string option list * attribute list -> state -> state
   18.52 +  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
   18.53 +  val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   18.54 +  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   18.55 +  val from_thmss: ((thm list * attribute list) list) list -> state -> state
   18.56 +  val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.57 +  val with_thmss: ((thm list * attribute list) list) list -> state -> state
   18.58 +  val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.59 +  val using: ((thm list * attribute list) list) list -> state -> state
   18.60 +  val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.61 +  val unfolding: ((thm list * attribute list) list) list -> state -> state
   18.62 +  val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   18.63 +  val invoke_case: string * string option list * attribute list -> state -> state
   18.64 +  val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
   18.65    val begin_block: state -> state
   18.66    val next_block: state -> state
   18.67    val end_block: state -> state
   18.68 @@ -87,9 +87,9 @@
   18.69      ((binding * 'a list) * 'b) list -> state -> state
   18.70    val local_qed: Method.text option * bool -> state -> state
   18.71    val theorem: Method.text option -> (thm list list -> context -> context) ->
   18.72 +    (term * term list) list list -> context -> state
   18.73 +  val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
   18.74      (string * string list) list list -> context -> state
   18.75 -  val theorem_i: Method.text option -> (thm list list -> context -> context) ->
   18.76 -    (term * term list) list list -> context -> state
   18.77    val global_qed: Method.text option * bool -> state -> context
   18.78    val local_terminal_proof: Method.text * Method.text option -> state -> state
   18.79    val local_default_proof: state -> state
   18.80 @@ -102,13 +102,13 @@
   18.81    val global_skip_proof: bool -> state -> context
   18.82    val global_done_proof: state -> context
   18.83    val have: Method.text option -> (thm list list -> state -> state) ->
   18.84 +    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   18.85 +  val have_cmd: Method.text option -> (thm list list -> state -> state) ->
   18.86      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   18.87 -  val have_i: Method.text option -> (thm list list -> state -> state) ->
   18.88 -    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   18.89    val show: Method.text option -> (thm list list -> state -> state) ->
   18.90 +    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   18.91 +  val show_cmd: Method.text option -> (thm list list -> state -> state) ->
   18.92      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   18.93 -  val show_i: Method.text option -> (thm list list -> state -> state) ->
   18.94 -    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   18.95    val schematic_goal: state -> bool
   18.96    val is_relevant: state -> bool
   18.97    val local_future_proof: (state -> ('a * state) Future.future) ->
   18.98 @@ -535,10 +535,10 @@
   18.99  
  18.100  in
  18.101  
  18.102 -val match_bind = gen_bind (ProofContext.match_bind false);
  18.103 -val match_bind_i = gen_bind (ProofContext.match_bind_i false);
  18.104 -val let_bind = gen_bind (ProofContext.match_bind true);
  18.105 -val let_bind_i = gen_bind (ProofContext.match_bind_i true);
  18.106 +val match_bind = gen_bind (ProofContext.match_bind_i false);
  18.107 +val match_bind_cmd = gen_bind (ProofContext.match_bind false);
  18.108 +val let_bind = gen_bind (ProofContext.match_bind_i true);
  18.109 +val let_bind_cmd = gen_bind (ProofContext.match_bind true);
  18.110  
  18.111  end;
  18.112  
  18.113 @@ -554,8 +554,8 @@
  18.114  
  18.115  in
  18.116  
  18.117 -val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
  18.118 -val fix_i = gen_fix (K I);
  18.119 +val fix = gen_fix (K I);
  18.120 +val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
  18.121  
  18.122  end;
  18.123  
  18.124 @@ -572,12 +572,12 @@
  18.125  
  18.126  in
  18.127  
  18.128 -val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
  18.129 -val assm_i    = gen_assume ProofContext.add_assms_i (K I);
  18.130 -val assume    = assm Assumption.assume_export;
  18.131 -val assume_i  = assm_i Assumption.assume_export;
  18.132 -val presume   = assm Assumption.presume_export;
  18.133 -val presume_i = assm_i Assumption.presume_export;
  18.134 +val assm = gen_assume ProofContext.add_assms_i (K I);
  18.135 +val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
  18.136 +val assume = assm Assumption.assume_export;
  18.137 +val assume_cmd = assm_cmd Assumption.assume_export;
  18.138 +val presume = assm Assumption.presume_export;
  18.139 +val presume_cmd = assm_cmd Assumption.presume_export;
  18.140  
  18.141  end;
  18.142  
  18.143 @@ -605,8 +605,8 @@
  18.144  
  18.145  in
  18.146  
  18.147 -val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
  18.148 -val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
  18.149 +val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
  18.150 +val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
  18.151  
  18.152  end;
  18.153  
  18.154 @@ -646,18 +646,18 @@
  18.155  
  18.156  in
  18.157  
  18.158 -val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
  18.159 -val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
  18.160 +val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
  18.161 +val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
  18.162  
  18.163 -val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  18.164 -val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
  18.165 +val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
  18.166 +val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  18.167  
  18.168 -val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  18.169 -val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
  18.170 +val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
  18.171 +val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  18.172  
  18.173  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
  18.174  
  18.175 -fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
  18.176 +fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
  18.177  
  18.178  end;
  18.179  
  18.180 @@ -686,10 +686,10 @@
  18.181  
  18.182  in
  18.183  
  18.184 -val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
  18.185 -val using_i = gen_using append_using (K (K I)) (K I) (K I);
  18.186 -val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
  18.187 -val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
  18.188 +val using = gen_using append_using (K (K I)) (K I) (K I);
  18.189 +val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
  18.190 +val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
  18.191 +val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
  18.192  
  18.193  end;
  18.194  
  18.195 @@ -709,15 +709,15 @@
  18.196      val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
  18.197    in
  18.198      state'
  18.199 -    |> assume_i assumptions
  18.200 +    |> assume assumptions
  18.201      |> bind_terms Auto_Bind.no_facts
  18.202 -    |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
  18.203 +    |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
  18.204    end;
  18.205  
  18.206  in
  18.207  
  18.208 -val invoke_case = gen_invoke_case Attrib.attribute;
  18.209 -val invoke_case_i = gen_invoke_case (K I);
  18.210 +val invoke_case = gen_invoke_case (K I);
  18.211 +val invoke_case_cmd = gen_invoke_case Attrib.attribute;
  18.212  
  18.213  end;
  18.214  
  18.215 @@ -901,8 +901,8 @@
  18.216    init ctxt
  18.217    |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
  18.218  
  18.219 -val theorem = global_goal ProofContext.bind_propp_schematic;
  18.220 -val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
  18.221 +val theorem = global_goal ProofContext.bind_propp_schematic_i;
  18.222 +val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
  18.223  
  18.224  fun global_qeds txt =
  18.225    end_proof true txt
  18.226 @@ -974,10 +974,10 @@
  18.227  
  18.228  in
  18.229  
  18.230 -val have = gen_have Attrib.attribute ProofContext.bind_propp;
  18.231 -val have_i = gen_have (K I) ProofContext.bind_propp_i;
  18.232 -val show = gen_show Attrib.attribute ProofContext.bind_propp;
  18.233 -val show_i = gen_show (K I) ProofContext.bind_propp_i;
  18.234 +val have = gen_have (K I) ProofContext.bind_propp_i;
  18.235 +val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
  18.236 +val show = gen_show (K I) ProofContext.bind_propp_i;
  18.237 +val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
  18.238  
  18.239  end;
  18.240  
    19.1 --- a/src/Pure/Isar/specification.ML	Sun Apr 25 15:13:33 2010 +0200
    19.2 +++ b/src/Pure/Isar/specification.ML	Sun Apr 25 15:52:03 2010 +0200
    19.3 @@ -403,7 +403,7 @@
    19.4      goal_ctxt
    19.5      |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
    19.6      |> snd
    19.7 -    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
    19.8 +    |> Proof.theorem before_qed after_qed' (map snd stmt)
    19.9      |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
   19.10      |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
   19.11          error "Illegal schematic goal statement")
    20.1 --- a/src/Pure/ML/ml_thms.ML	Sun Apr 25 15:13:33 2010 +0200
    20.2 +++ b/src/Pure/ML/ml_thms.ML	Sun Apr 25 15:52:03 2010 +0200
    20.3 @@ -64,7 +64,7 @@
    20.4          fun after_qed res goal_ctxt =
    20.5            put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
    20.6          val ctxt' = ctxt
    20.7 -          |> Proof.theorem_i NONE after_qed propss
    20.8 +          |> Proof.theorem NONE after_qed propss
    20.9            |> Proof.global_terminal_proof methods;
   20.10          val (a, background') = background
   20.11            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    21.1 --- a/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:13:33 2010 +0200
    21.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:52:03 2010 +0200
    21.3 @@ -574,7 +574,7 @@
    21.4        val prop_src =
    21.5          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
    21.6        val _ = context
    21.7 -        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
    21.8 +        |> Proof.theorem NONE (K I) [[(prop, [])]]
    21.9          |> Proof.global_terminal_proof methods;
   21.10      in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
   21.11