# HG changeset patch
# User wenzelm
# Date 1570824409 -7200
# Node ID 3d8953224f33e147187ce88cc5369d516f127872
# Parent  77c8b8e73f883e46182b3e0da59601f63c99271a# Parent  5b80eb4fd0f30752561fee6d82acaee9feaae454
merged

diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Extraction.thy	Fri Oct 11 22:06:49 2019 +0200
@@ -17,11 +17,11 @@
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
     Proofterm.rewrite_proof_notypes
-      ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
+      ([], Rewrite_HOL_Proof.elim_cong :: Proof_Rewrite_Rules.rprocs true) o
     Proofterm.rewrite_proof thy
-      (RewriteHOLProof.rews,
-       ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
-    ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
+      (Rewrite_HOL_Proof.rews,
+       Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]) o
+    Proof_Rewrite_Rules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
 \<close>
 
 lemmas [extraction_expand] =
diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Proofs/ex/Proof_Terms.thy
--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Oct 11 22:06:49 2019 +0200
@@ -23,14 +23,14 @@
   val thm = @{thm ex};
 
   (*proof body with digest*)
-  val body = Proofterm.strip_thm (Thm.proof_body_of thm);
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
 
   (*proof term only*)
   val prf = Proofterm.proof_of body;
 
   (*clean output*)
-  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> false thm);
-  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> true thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
 
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Oct 11 22:06:49 2019 +0200
@@ -13,7 +13,8 @@
 
 ML \<open>
   fun export_proof thy thm =
-    Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm);
+    Proofterm.encode (Sign.consts_of thy)
+      (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm));
 
   fun import_proof thy xml =
     let
diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -117,7 +117,7 @@
     NONE => NONE
   | SOME body =>
     let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
-      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
+      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body))
       handle TOO_MANY () => NONE
     end)
 
diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -269,7 +269,7 @@
   in (name, (vs,
     if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     Extraction.abs_corr_shyps thy rule vs vs2
-      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
+      (Proof_Rewrite_Rules.un_hhf_proof rlz' (attach_typeS rlz)
          (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
   end;
 
diff -r 77c8b8e73f88 -r 3d8953224f33 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -10,7 +10,7 @@
   val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
 end;
 
-structure RewriteHOLProof : REWRITE_HOL_PROOF =
+structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF =
 struct
 
 val rews =
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -250,7 +250,7 @@
     | SOME srcs =>
         let
           val ctxt = Toplevel.context_of state;
-          val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
+          val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full;
         in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
 
 fun string_of_prop ctxt s =
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/PIDE/xml.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -11,6 +11,7 @@
   type 'a A
   type 'a T
   type 'a V
+  type 'a P
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
@@ -290,6 +291,7 @@
 type 'a A = 'a -> string;
 type 'a T = 'a -> body;
 type 'a V = 'a -> string list * body;
+type 'a P = 'a -> string list;
 
 
 (* atomic values *)
@@ -347,6 +349,7 @@
 type 'a A = string -> 'a;
 type 'a T = body -> 'a;
 type 'a V = string list * body -> 'a;
+type 'a P = string list -> 'a;
 
 
 (* atomic values *)
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Oct 11 22:06:49 2019 +0200
@@ -241,6 +241,7 @@
   {
     type T[A] = A => XML.Body
     type V[A] = PartialFunction[A, (List[String], XML.Body)]
+    type P[A] = PartialFunction[A, List[String]]
 
 
     /* atomic values */
@@ -309,6 +310,7 @@
   {
     type T[A] = XML.Body => A
     type V[A] = (List[String], XML.Body) => A
+    type P[A] = PartialFunction[List[String], A]
 
 
     /* atomic values */
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -177,7 +177,7 @@
   let
     val (oracles, thms) =
       ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
-        (fn Oracle (name, prop, _) => apfst (cons (name, prop))
+        (fn Oracle (name, prop, _) => apfst (cons (name, SOME prop))
           | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
           | _ => I);
     val body =
@@ -505,7 +505,7 @@
     val rtypes = map fst types;
     val typroc = typeof_proc [];
     val prep = the_default (K I) prep thy' o
-      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
+      Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
       Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 
@@ -529,7 +529,7 @@
       Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
 
     fun mk_sprfs cs tye = maps (fn (_, T) =>
-      ProofRewriteRules.mk_of_sort_proof thy' (map SOME cs)
+      Proof_Rewrite_Rules.expand_of_sort_proof thy' (map SOME cs)
         (T, Sign.defaultS thy)) tye;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -137,6 +137,13 @@
 
           | thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
 
+          | thm_of _ _ (OfClass (T, c)) =
+              if Sign.of_sort thy (T, [c])
+              then Thm.of_class (Thm.global_ctyp_of thy T, c)
+              else
+                error ("thm_of_proof: bad OfClass proof " ^
+                  Syntax.string_of_term_global thy (Logic.mk_of_class (T, c)))
+
           | thm_of _ _ _ = error "thm_of_proof: partial proof term";
 
       in beta_eta_convert (thm_of ([], prf_names) [] prf) end
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -14,12 +14,13 @@
   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
   val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
   val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
-  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+  val expand_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+  val expand_of_class_proof : theory -> term option list -> typ * class -> proof
   val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
     (Proofterm.proof * Proofterm.proof) option
 end;
 
-structure ProofRewriteRules : PROOF_REWRITE_RULES =
+structure Proof_Rewrite_Rules : PROOF_REWRITE_RULES =
 struct
 
 fun rew b _ _ =
@@ -255,20 +256,22 @@
     val defs' = map (Logic.dest_equals o
       map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
     val defnames = map Thm.derivation_name defs;
-    val f = if not r then I else
-      let
-        val cnames = map (fst o dest_Const o fst) defs';
-        val thms = Proofterm.fold_proof_atoms true
-          (fn PThm ({name, prop, ...}, _) =>
-              if member (op =) defnames name orelse
-                not (exists_Const (member (op =) cnames o #1) prop)
-              then I
-              else cons (name, SOME prop)
-            | _ => I) [prf] [];
-      in Proofterm.expand_proof thy thms end;
+    val prf' =
+      if r then
+        let
+          val cnames = map (fst o dest_Const o fst) defs';
+          val thms = Proofterm.fold_proof_atoms true
+            (fn PThm ({name, prop, ...}, _) =>
+                if member (op =) defnames name orelse
+                  not (exists_Const (member (op =) cnames o #1) prop)
+                then I
+                else cons (name, SOME prop)
+              | _ => I) [prf] [];
+        in Proofterm.expand_proof thy thms prf end
+      else prf;
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])
-      (fst (insert_refl defnames [] (f prf)))
+      (fst (insert_refl defnames [] prf'))
   end;
 
 
@@ -340,33 +343,35 @@
 
 (**** expand OfClass proofs ****)
 
-fun mk_of_sort_proof thy hs (T, S) =
+fun expand_of_sort_proof thy hyps (T, S) =
   let
-    val hs' = map
-      (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
-        | NONE => NONE) hs;
-    val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
+    val of_class_hyps = map (fn SOME t => try Logic.dest_of_class t | NONE => NONE) hyps;
+    fun of_class_index p =
+      (case find_index (fn SOME h => h = p | NONE => false) of_class_hyps of
+        ~1 => raise Fail "expand_of_class_proof: missing class hypothesis"
+      | i => PBound i);
+
+    val sorts = AList.coalesce (op =) (rev (map_filter I of_class_hyps));
     fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
     val subst = map_atyps
-      (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
-        | T as TFree (s, _) => TFree (s, get_sort T));
-    fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
-        ~1 => error "expand_of_class: missing class hypothesis"
-      | i => PBound i;
-    fun reconstruct prf prop = prf |>
-      Proofterm.reconstruct_proof thy prop |>
-      Proofterm.expand_proof thy [("", NONE)] |>
-      Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
+      (fn T as TVar (ai, _) => TVar (ai, get_sort T)
+        | T as TFree (a, _) => TFree (a, get_sort T));
+
+    fun reconstruct prop =
+      Proofterm.reconstruct_proof thy prop #>
+      Proofterm.expand_proof thy [("", NONE)] #>
+      Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
   in
-    map2 reconstruct
+    map2 reconstruct (Logic.mk_of_sort (T, S))
       (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
         (OfClass o apfst Type.strip_sorts) (subst T, S))
-      (Logic.mk_of_sort (T, S))
   end;
 
-fun expand_of_class thy Ts hs (OfClass (T, c)) =
-      mk_of_sort_proof thy hs (T, [c]) |>
-      hd |> rpair Proofterm.no_skel |> SOME
-  | expand_of_class thy Ts hs _ = NONE;
+fun expand_of_class_proof thy hyps (T, c) =
+  hd (expand_of_sort_proof thy hyps (T, [c]));
+
+fun expand_of_class thy (_: typ list) hyps (OfClass (T, c)) =
+      SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
+  | expand_of_class _ _ _ _ = NONE;
 
 end;
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -13,7 +13,7 @@
   val proof_syntax: Proofterm.proof -> theory -> theory
   val proof_of: bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
-  val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
+  val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
 structure Proof_Syntax : PROOF_SYNTAX =
@@ -195,7 +195,7 @@
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     (Proofterm.term_of_proof prf);
 
-fun pretty_clean_proof_of ctxt full thm =
-  pretty_proof ctxt (Thm.clean_proof_of full thm);
+fun pretty_standard_proof_of ctxt full thm =
+  pretty_proof ctxt (Thm.standard_proof_of full thm);
 
 end;
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -57,7 +57,7 @@
   let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
-fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full;
 
 fun pretty_theory ctxt (name, pos) =
   (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -271,7 +271,7 @@
       in
         (prop, (deps, proof)) |>
           let open XML.Encode Term_XML.Encode
-          in pair encode_prop (pair (list string) (option (Proofterm.encode_full consts))) end
+          in pair encode_prop (pair (list string) (option (Proofterm.encode_standard consts))) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -105,7 +105,7 @@
     val used =
       Proofterm.fold_body_thms
         (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
-        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+        (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
         Symtab.empty;
 
     fun is_unused a = not (Symtab.defined used a);
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/logic.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -62,7 +62,6 @@
     constraints_map: (sort * typ) list,
     atyp_map: typ -> typ,
     map_atyps: typ -> typ,
-    map_atyps': typ -> typ,
     constraints: ((typ * class) * term) list,
     outer_constraints: (typ * class) list};
   val unconstrainT: sort list -> term -> unconstrain_context * term
@@ -355,7 +354,6 @@
   constraints_map: (sort * typ) list,
   atyp_map: typ -> typ,
   map_atyps: typ -> typ,
-  map_atyps': typ -> typ,
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
@@ -373,9 +371,6 @@
       map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
-    val present_map' = map (fn (T, T') => (Type.strip_sorts T', T)) present_map;
-    val constraints_map' = map (fn (S, T') => (Type.strip_sorts T', dummy_tfree S)) constraints_map;
-
     fun atyp_map T =
       (case AList.lookup (op =) present_map T of
         SOME U => U
@@ -384,16 +379,7 @@
             SOME U => U
           | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
 
-    fun atyp_map' T =
-      (case AList.lookup (op =) present_map' T of
-        SOME U => U
-      | NONE =>
-          (case AList.lookup (op =) constraints_map' T of
-            SOME U => U
-          | NONE => raise TYPE ("Dangling type variable", [T], [prop])));
-
     val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
-    val map_atyps' = Term.map_atyps atyp_map';
 
     val constraints =
       constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
@@ -407,7 +393,6 @@
       constraints_map = constraints_map,
       atyp_map = atyp_map,
       map_atyps = map_atyps,
-      map_atyps' = map_atyps',
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -114,7 +114,7 @@
   val untag: string -> attribute
   val kind: string -> attribute
   val reconstruct_proof_of: thm -> Proofterm.proof
-  val clean_proof_of: bool -> thm -> Proofterm.proof
+  val standard_proof_of: bool -> thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts: bool Config.T
@@ -656,16 +656,10 @@
 fun reconstruct_proof_of thm =
   Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
-fun clean_proof_of full thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val (_, prop) =
-      Logic.unconstrainT (Thm.shyps_of thm)
-        (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
-  in
-    Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
-    |> Proofterm.reconstruct_proof thy prop
-    |> Proofterm.expand_proof thy [("", NONE)]
+fun standard_proof_of full thm =
+  let val thy = Thm.theory_of_thm thm in
+    reconstruct_proof_of thm
+    |> Proofterm.expand_proof thy [("", NONE), (Thm.raw_derivation_name thm, NONE)]
     |> Proofterm.rew_proof thy
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -23,7 +23,7 @@
    | Hyp of term
    | PAxm of string * term * typ list option
    | OfClass of typ * class
-   | Oracle of string * term option * typ list option
+   | Oracle of string * term * typ list option
    | PThm of thm_header * thm_body
   and proof_body = PBody of
     {oracles: (string * term option) Ord_List.T,
@@ -61,7 +61,7 @@
 
   val encode: Consts.T -> proof XML.Encode.T
   val encode_body: Consts.T -> proof_body XML.Encode.T
-  val encode_full: Consts.T -> proof XML.Encode.T
+  val encode_standard: Consts.T -> proof XML.Encode.T
   val decode: Consts.T -> proof XML.Decode.T
   val decode_body: Consts.T -> proof_body XML.Decode.T
 
@@ -77,7 +77,7 @@
   val proof_combP: proof * proof list -> proof
   val strip_combt: proof -> proof * term option list
   val strip_combP: proof -> proof * proof list
-  val strip_thm: proof_body -> proof_body
+  val strip_thm_body: proof_body -> proof_body
   val map_proof_same: term Same.operation -> typ Same.operation
     -> (typ * class -> proof) -> proof Same.operation
   val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
@@ -103,21 +103,22 @@
   val term_of_proof: proof -> term
 
   (*proof terms for specific inference rules*)
+  val trivial_proof: proof
   val implies_intr_proof: term -> proof -> proof
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
-  val rotate_proof: term list -> term -> int -> proof -> proof
+  val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
-  val generalize: string list * string list -> int -> proof -> proof
+  val generalize_proof: string list * string list -> int -> term -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
-  val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
+  val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
     int -> int -> proof -> proof -> proof
   val equality_axms: (string * term) list
   val reflexive_axm: proof
@@ -141,7 +142,7 @@
     (string * class list list * class -> proof) ->
     (typ * class -> proof) -> typ * sort -> proof list
   val axm_proof: string -> term -> proof
-  val oracle_proof: string -> term -> oracle * proof
+  val oracle_proof: string -> term -> proof
   val shrink_proof: proof -> proof
 
   (*rewriting on proof terms*)
@@ -196,7 +197,7 @@
  | Hyp of term
  | PAxm of string * term * typ list option
  | OfClass of typ * class
- | Oracle of string * term option * typ list option
+ | Oracle of string * term * typ list option
  | PThm of thm_header * thm_body
 and proof_body = PBody of
   {oracles: (string * term option) Ord_List.T,
@@ -210,7 +211,6 @@
 
 type oracle = string * term option;
 val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
-val oracle_prop = the_default Term.dummy;
 
 type thm = serial * thm_node;
 val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
@@ -337,7 +337,7 @@
   fn Hyp a => ([], term consts a),
   fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn OfClass (a, b) => ([b], typ a),
-  fn Oracle (a, b, c) => ([a], pair (option (term consts)) (option (list typ)) (b, c)),
+  fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
     ([int_atom serial, theory_name, name],
       pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
@@ -350,17 +350,17 @@
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
-fun full_proof consts prf = prf |> variant
+fun standard_proof consts prf = prf |> variant
  [fn MinProof => ([], []),
   fn PBound a => ([int_atom a], []),
-  fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)),
-  fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)),
+  fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (standard_proof consts) (b, c)),
+  fn a % SOME b => ([], pair (standard_proof consts) (term consts) (a, b)),
+  fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
   fn Hyp a => ([], term consts a),
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   fn OfClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair (option (term consts)) (list typ) (prop, Ts)),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair (term consts) (list typ) (prop, Ts)),
   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
     ([int_atom serial, theory_name, name], list typ Ts)];
 
@@ -368,7 +368,7 @@
 
 val encode = proof;
 val encode_body = proof_body;
-val encode_full = full_proof;
+val encode_standard = standard_proof;
 
 end;
 
@@ -389,8 +389,7 @@
   fn ([], a) => Hyp (term consts a),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
   fn ([b], a) => OfClass (typ a, b),
-  fn ([a], b) =>
-    let val (c, d) = pair (option (term consts)) (option (list typ)) b in Oracle (a, c, d) end,
+  fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b, c], d) =>
     let
       val ((e, (f, (g, h)))) =
@@ -450,13 +449,13 @@
           | stripc  x =  x
     in  stripc (prf, [])  end;
 
-fun strip_thm (body as PBody {proof, ...}) =
+fun strip_thm_body (body as PBody {proof, ...}) =
   (case fst (strip_combt (fst (strip_combP proof))) of
     PThm (_, Thm_Body {body = body', ...}) => Future.join body'
   | _ => body);
 
-val mk_Abst = fold_rev (fn (s, _: typ) => fn prf => Abst (s, NONE, prf));
-fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
+val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf));
+val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf));
 
 fun map_proof_same term typ ofclass =
   let
@@ -832,7 +831,7 @@
         val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
       in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
   | term_of _ (Hyp t) = Hypt $ t
-  | term_of _ (Oracle (_, t, _)) = Oraclet $ oracle_prop t
+  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
   | term_of _ MinProof = MinProoft;
 
 in
@@ -845,6 +844,11 @@
 
 (** inference rules **)
 
+(* trivial implication *)
+
+val trivial_proof = AbsP ("H", NONE, PBound 0);
+
+
 (* implication introduction *)
 
 fun gen_implies_intr_proof f h prf =
@@ -921,35 +925,44 @@
 
 (* rotate assumptions *)
 
-fun rotate_proof Bs Bi m prf =
+fun rotate_proof Bs Bi' params asms m prf =
   let
-    val params = Term.strip_all_vars Bi;
-    val asms = Logic.strip_imp_prems (Term.strip_all_body Bi);
     val i = length asms;
     val j = length Bs;
   in
-    mk_AbsP (j+1, proof_combP (prf, map PBound
-      (j downto 1) @ [mk_Abst params (mk_AbsP (i,
-        proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
+    mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound
+      (j downto 1) @ [mk_Abst params (mk_AbsP asms
+        (proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
           map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   end;
 
 
 (* permute premises *)
 
-fun permute_prems_proof prems j k prf =
-  let val n = length prems
-  in mk_AbsP (n, proof_combP (prf,
-    map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+fun permute_prems_proof prems' j k prf =
+  let val n = length prems' in
+    mk_AbsP prems'
+      (proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
   end;
 
 
 (* generalization *)
 
-fun generalize (tfrees, frees) idx =
-  Same.commit (map_proof_terms_same
-    (Term_Subst.generalize_same (tfrees, frees) idx)
-    (Term_Subst.generalizeT_same tfrees idx));
+fun generalize_proof (tfrees, frees) idx prop prf =
+  let
+    val gen =
+      if null frees then []
+      else
+        fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I)
+          (Term_Subst.generalize (tfrees, []) idx prop) [];
+  in
+    prf
+    |> Same.commit (map_proof_terms_same
+        (Term_Subst.generalize_same (tfrees, []) idx)
+        (Term_Subst.generalizeT_same tfrees idx))
+    |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
+    |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
+  end;
 
 
 (* instantiation *)
@@ -1003,7 +1016,7 @@
             map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
               (i + k - 1 downto i));
   in
-    mk_AbsP (k, lift [] [] 0 0 Bi)
+    mk_AbsP ps (lift [] [] 0 0 Bi)
   end;
 
 fun incr_indexes i =
@@ -1023,8 +1036,7 @@
   in all_prf t end;
 
 fun assumption_proof Bs Bi n prf =
-  mk_AbsP (length Bs, proof_combP (prf,
-    map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
+  mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
 
 
 (* composition of object rule with proof state *)
@@ -1036,12 +1048,12 @@
   | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
       map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
 
-fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf =
+fun bicompose_proof flatten Bs As A oldAs n m rprf sprf =
   let
-    val la = length newAs;
     val lb = length Bs;
+    val la = length As;
   in
-    mk_AbsP (lb+la, proof_combP (sprf,
+    mk_AbsP (Bs @ As) (proof_combP (sprf,
       map PBound (lb + la - 1 downto la)) %%
         proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
           map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
@@ -1146,13 +1158,15 @@
     val frees = map SOME (frees_of prop);
   in vars @ frees end;
 
-fun axm_proof name prop =
-  proof_combt' (PAxm (name, prop, NONE), prop_args prop);
+fun const_proof mk name prop =
+  let
+    val args = prop_args prop;
+    val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
+    val head = mk (name, prop1, NONE);
+  in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end;
 
-fun oracle_proof name prop =
-  if ! proofs = 0
-  then ((name, NONE), Oracle (name, NONE, NONE))
-  else ((name, SOME prop), proof_combt' (Oracle (name, SOME prop, NONE), prop_args prop));
+val axm_proof = const_proof PAxm;
+val oracle_proof = const_proof Oracle;
 
 val shrink_proof =
   let
@@ -1191,7 +1205,7 @@
             val prop =
               (case prf of
                 PAxm (_, prop, _) => prop
-              | Oracle (_, prop, _) => oracle_prop prop
+              | Oracle (_, prop, _) => prop
               | PThm ({prop, ...}, _) => prop
               | _ => raise Fail "shrink: proof not in normal form");
             val vs = vars_of prop;
@@ -1786,7 +1800,7 @@
       | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
           mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
-          mk_cnstrts_atom env vTs (oracle_prop prop) opTs prf
+          mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
       | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF ()
   in mk_cnstrts env [] [] Symtab.empty cprf end;
@@ -1882,7 +1896,7 @@
   | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
   | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c)
-  | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom (oracle_prop prop) Ts
+  | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
@@ -1893,45 +1907,45 @@
 
 fun expand_proof thy thms prf =
   let
-    fun expand maxidx prfs (AbsP (s, t, prf)) =
-          let val (maxidx', prfs', prf') = expand maxidx prfs prf
-          in (maxidx', prfs', AbsP (s, t, prf')) end
-      | expand maxidx prfs (Abst (s, T, prf)) =
-          let val (maxidx', prfs', prf') = expand maxidx prfs prf
-          in (maxidx', prfs', Abst (s, T, prf')) end
-      | expand maxidx prfs (prf1 %% prf2) =
-          let
-            val (maxidx', prfs', prf1') = expand maxidx prfs prf1;
-            val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2;
-          in (maxidx'', prfs'', prf1' %% prf2') end
-      | expand maxidx prfs (prf % t) =
-          let val (maxidx', prfs', prf') = expand maxidx prfs prf
-          in (maxidx', prfs', prf' % t) end
-      | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
-          if not (exists
-            (fn (b, NONE) => a = b
-              | (b, SOME prop') => a = b andalso prop = prop') thms)
-          then (maxidx, prfs, prf) else
+    fun do_expand a prop =
+      exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms;
+
+    fun expand seen maxidx (AbsP (s, t, prf)) =
+          let val (seen', maxidx', prf') = expand seen maxidx prf
+          in (seen', maxidx', AbsP (s, t, prf')) end
+      | expand seen maxidx (Abst (s, T, prf)) =
+          let val (seen', maxidx', prf') = expand seen maxidx prf
+          in (seen', maxidx', Abst (s, T, prf')) end
+      | expand seen maxidx (prf1 %% prf2) =
           let
-            val (maxidx', prf, prfs') =
-              (case AList.lookup (op =) prfs (a, prop) of
-                NONE =>
-                  let
-                    val prf' =
-                      thm_body_proof_open thm_body
-                      |> reconstruct_proof thy prop
-                      |> forall_intr_vfs_prf prop;
-                    val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
-                  in
-                    (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
-                      ((a, prop), (maxidx', prf)) :: prfs')
-                  end
-              | SOME (maxidx', prf) =>
-                  (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
-          in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end
-      | expand maxidx prfs prf = (maxidx, prfs, prf);
+            val (seen', maxidx', prf1') = expand seen maxidx prf1;
+            val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2;
+          in (seen'', maxidx'', prf1' %% prf2') end
+      | expand seen maxidx (prf % t) =
+          let val (seen', maxidx', prf') = expand seen maxidx prf
+          in (seen', maxidx', prf' % t) end
+      | expand seen maxidx (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
+          if do_expand a prop then
+            let
+              val (seen', maxidx', prf') =
+                (case AList.lookup (op =) seen (a, prop) of
+                  NONE =>
+                    let
+                      val prf1 =
+                        thm_body_proof_open thm_body
+                        |> reconstruct_proof thy prop
+                        |> forall_intr_vfs_prf prop;
+                      val (seen1, maxidx1, prf2) = expand_init seen prf1
+                      val seen2 = ((a, prop), (maxidx1, prf2)) :: seen1;
+                    in (seen2, maxidx1, prf2) end
+                | SOME (maxidx1, prf1) => (seen, maxidx1, prf1));
+              val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts;
+            in (seen', maxidx' + maxidx + 1, prf'') end
+          else (seen, maxidx, prf)
+      | expand seen maxidx prf = (seen, maxidx, prf)
+    and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf;
 
-  in #3 (expand (maxidx_proof prf ~1) [] prf) end;
+  in #3 (expand_init [] prf) end;
 
 end;
 
@@ -2068,7 +2082,7 @@
     val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
     fun ofclass (ty, c) =
       let val ty' = Term.map_atyps (#atyp_map ucontext) ty;
-      in the_single (of_sort_proof algebra classrel_proof arity_proof  hyp_map (ty', [c])) end;
+      in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end;
   in
     Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
     #> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
@@ -2078,7 +2092,7 @@
 
 fun encode_export consts prop prf =
   let open XML.Encode Term_XML.Encode
-  in pair (term consts) (encode_full consts) (prop, prf) end;
+  in pair (term consts) (encode_standard consts) (prop, prf) end;
 
 fun export_proof thy i prop prf =
   let
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/term.scala
--- a/src/Pure/term.scala	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term.scala	Fri Oct 11 22:06:49 2019 +0200
@@ -57,7 +57,7 @@
   case class Hyp(hyp: Term) extends Proof
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class OfClass(typ: Typ, cls: String) extends Proof
-  case class Oracle(name: String, prop: Option[Term], types: List[Typ]) extends Proof
+  case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
   case class PThm(serial: Long, theory_name: String, approximative_name: String, types: List[Typ])
     extends Proof
 
@@ -153,7 +153,7 @@
               case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
               case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
-                store(Oracle(cache_string(name), prop.map(cache_term(_)), cache_typs(types)))
+                store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
               case PThm(serial, theory_name, name, types) =>
                 store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
             }
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term_xml.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -7,10 +7,13 @@
 signature TERM_XML_OPS =
 sig
   type 'a T
+  type 'a P
+  val indexname: indexname P
   val sort: sort T
+  val typ_raw: typ T
+  val term_raw: term T
   val typ: typ T
   val term: Consts.T -> term T
-  val term_raw: term T
 end
 
 signature TERM_XML =
@@ -27,29 +30,33 @@
 
 open XML.Encode;
 
+fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
+
 val sort = list string;
 
-fun typ T = T |> variant
- [fn Type (a, b) => ([a], list typ b),
+fun typ_raw T = T |> variant
+ [fn Type (a, b) => ([a], list typ_raw b),
   fn TFree (a, b) => ([a], sort b),
-  fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
+  fn TVar (a, b) => (indexname a, sort b)];
+
+fun term_raw t = t |> variant
+ [fn Const (a, b) => ([a], typ_raw b),
+  fn Free (a, b) => ([a], typ_raw b),
+  fn Var (a, b) => (indexname a, typ_raw b),
+  fn Bound a => ([int_atom a], []),
+  fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+  fn op $ a => ([], pair term_raw term_raw a)];
+
+fun typ T = option typ_raw (if T = dummyT then NONE else SOME T);
 
 fun term consts t = t |> variant
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
   fn Free (a, b) => ([a], typ b),
-  fn Var ((a, b), c) => ([a, int_atom b], typ c),
+  fn Var (a, b) => (indexname a, typ b),
   fn Bound a => ([int_atom a], []),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn op $ a => ([], pair (term consts) (term consts) a)];
 
-fun term_raw t = t |> variant
- [fn Const (a, b) => ([a], typ b),
-  fn Free (a, b) => ([a], typ b),
-  fn Var ((a, b), c) => ([a, int_atom b], typ c),
-  fn Bound a => ([int_atom a], []),
-  fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
-  fn op $ a => ([], pair term_raw term_raw a)];
-
 end;
 
 structure Decode =
@@ -57,29 +64,34 @@
 
 open XML.Decode;
 
+fun indexname [a] = (a, 0)
+  | indexname [a, b] = (a, int_atom b);
+
 val sort = list string;
 
-fun typ T = T |> variant
- [fn ([a], b) => Type (a, list typ b),
+fun typ_raw body = body |> variant
+ [fn ([a], b) => Type (a, list typ_raw b),
   fn ([a], b) => TFree (a, sort b),
-  fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
+  fn (a, b) => TVar (indexname a, sort b)];
 
-fun term consts t = t |> variant
+fun term_raw body = body |> variant
+ [fn ([a], b) => Const (a, typ_raw b),
+  fn ([a], b) => Free (a, typ_raw b),
+  fn (a, b) => Var (indexname a, typ_raw b),
+  fn ([a], []) => Bound (int_atom a),
+  fn ([a], b) => let val (c, d) = pair typ_raw term_raw b in Abs (a, c, d) end,
+  fn ([], a) => op $ (pair term_raw term_raw a)];
+
+val typ = option typ_raw #> the_default dummyT;
+
+fun term consts body = body |> variant
  [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
   fn ([a], b) => Free (a, typ b),
-  fn ([a, b], c) => Var ((a, int_atom b), typ c),
+  fn (a, b) => Var (indexname a, typ b),
   fn ([a], []) => Bound (int_atom a),
   fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair (term consts) (term consts) a)];
 
-fun term_raw t = t |> variant
- [fn ([a], b) => Const (a, typ b),
-  fn ([a], b) => Free (a, typ b),
-  fn ([a, b], c) => Var ((a, int_atom b), typ c),
-  fn ([a], []) => Bound (int_atom a),
-  fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
-  fn ([], a) => op $ (pair term_raw term_raw a)];
-
 end;
 
 end;
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term_xml.scala	Fri Oct 11 22:06:49 2019 +0200
@@ -15,19 +15,26 @@
   {
     import XML.Encode._
 
+    val indexname: P[Indexname] =
+      { case Indexname(a, 0) => List(a)
+        case Indexname(a, b) => List(a, int_atom(b)) }
+
     val sort: T[Sort] = list(string)
 
-    def typ: T[Typ] =
+    def typ_raw: T[Typ] =
       variant[Typ](List(
-        { case Type(a, b) => (List(a), list(typ)(b)) },
+        { case Type(a, b) => (List(a), list(typ_raw)(b)) },
         { case TFree(a, b) => (List(a), sort(b)) },
-        { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+        { case TVar(a, b) => (indexname(a), sort(b)) }))
+
+    val typ: T[Typ] =
+      { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
 
     def term: T[Term] =
       variant[Term](List(
         { case Const(a, b) => (List(a), list(typ)(b)) },
         { case Free(a, b) => (List(a), typ(b)) },
-        { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
+        { case Var(a, b) => (indexname(a), typ(b)) },
         { case Bound(a) => (List(int_atom(a)), Nil) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -37,19 +44,25 @@
   {
     import XML.Decode._
 
+    val indexname: P[Indexname] =
+      { case List(a) => Indexname(a, 0)
+        case List(a, b) => Indexname(a, int_atom(b)) }
+
     val sort: T[Sort] = list(string)
 
-    def typ: T[Typ] =
+    def typ_raw: T[Typ] =
       variant[Typ](List(
-        { case (List(a), b) => Type(a, list(typ)(b)) },
+        { case (List(a), b) => Type(a, list(typ_raw)(b)) },
         { case (List(a), b) => TFree(a, sort(b)) },
-        { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
+        { case (a, b) => TVar(indexname(a), sort(b)) }))
+
+    def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
 
     def term: T[Term] =
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) },
         { case (List(a), b) => Free(a, typ(b)) },
-        { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
+        { case (a, b) => Var(indexname(a), typ(b)) },
         { case (List(a), Nil) => Bound(int_atom(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
@@ -65,7 +78,7 @@
         { case (Nil, a) => Hyp(term(a)) },
         { case (List(a), b) => PAxm(a, list(typ)(b)) },
         { case (List(a), b) => OfClass(typ(b), a) },
-        { case (List(a), b) => val (c, d) = pair(option(term), list(typ))(b); Oracle(a, c, d) },
+        { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
         { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
   }
 }
diff -r 77c8b8e73f88 -r 3d8953224f33 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/thm.ML	Fri Oct 11 22:06:49 2019 +0200
@@ -713,6 +713,9 @@
 
 val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
+fun bad_proofs i =
+  error ("Illegal level of detail for proof objects: " ^ string_of_int i);
+
 fun deriv_rule2 f
     (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
     (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
@@ -725,7 +728,7 @@
         2 => f prf1 prf2
       | 1 => MinProof
       | 0 => MinProof
-      | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
+      | i => bad_proofs i);
   in make_deriv ps oracles thms prf end;
 
 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
@@ -1043,7 +1046,14 @@
         if T <> propT then
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
-          let val (oracle, prf) = Proofterm.oracle_proof name prop in
+          let
+            val (oracle, prf) =
+              (case ! Proofterm.proofs of
+                2 => ((name, SOME prop), Proofterm.oracle_proof name prop)
+              | 1 => ((name, SOME prop), MinProof)
+              | 0 => ((name, NONE), MinProof)
+              | i => bad_proofs i);
+          in
             Thm (make_deriv [] [oracle] [] prf,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),
               tags = [],
@@ -1496,12 +1506,12 @@
         val _ = exists bad_term hyps andalso
           raise THM ("generalize: variable free in assumptions", 0, [th]);
 
-        val gen = Term_Subst.generalize (tfrees, frees) idx;
-        val prop' = gen prop;
-        val tpairs' = map (apply2 gen) tpairs;
+        val generalize = Term_Subst.generalize (tfrees, frees) idx;
+        val prop' = generalize prop;
+        val tpairs' = map (apply2 generalize) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
       in
-        Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
+        Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
          {cert = cert,
           tags = [],
           maxidx = maxidx',
@@ -1631,7 +1641,7 @@
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
+    Thm (deriv_rule0 (fn () => Proofterm.trivial_proof),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1828,23 +1838,24 @@
     val (context, cert') = make_context_certificate [state] opt_ctxt cert;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
-      Thm (deriv_rule1
-          ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
-            Proofterm.assumption_proof Bs Bi n) der,
-       {tags = [],
-        maxidx = Envir.maxidx_of env,
-        constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
-        shyps = Envir.insert_sorts env shyps,
-        hyps = hyps,
-        tpairs =
-          if Envir.is_empty env then tpairs
-          else map (apply2 (Envir.norm_term env)) tpairs,
-        prop =
-          if Envir.is_empty env then (*avoid wasted normalizations*)
-            Logic.list_implies (Bs, C)
-          else (*normalize the new rule fully*)
-            Envir.norm_term env (Logic.list_implies (Bs, C)),
-        cert = cert'});
+      let
+        val normt = Envir.norm_term env;
+        fun assumption_proof prf =
+          Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
+      in
+        Thm (deriv_rule1
+          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
+         {tags = [],
+          maxidx = Envir.maxidx_of env,
+          constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
+          shyps = Envir.insert_sorts env shyps,
+          hyps = hyps,
+          tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
+          prop =
+            if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*)
+            else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*),
+          cert = cert'})
+      end;
 
     val (close, asms, concl) = Logic.assum_problems (~1, Bi);
     val concl' = close concl;
@@ -1898,7 +1909,7 @@
         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
-    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
+    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1923,14 +1934,16 @@
       handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
     val n_j = length moved_prems;
     val m = if k < 0 then n_j + k else k;
-    val prop' =
-      if 0 = m orelse m = n_j then prop
+    val (prems', prop') =
+      if 0 = m orelse m = n_j then (prems, prop)
       else if 0 < m andalso m < n_j then
-        let val (ps, qs) = chop m moved_prems
-        in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
+        let
+          val (ps, qs) = chop m moved_prems;
+          val prems' = fixed_prems @ qs @ ps;
+        in (prems', Logic.list_implies (prems', concl)) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
+    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -2079,14 +2092,14 @@
            val constraints' =
              union_constraints constraints1 constraints2
              |> insert_constraints_env (Context.certificate_theory cert) env;
+           fun bicompose_proof prf1 prf2 =
+             Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1)
+               prf1 prf2
            val th =
              Thm (deriv_rule2
-                   ((if Envir.is_empty env then I
-                     else if Envir.above env smax then
-                       (fn f => fn der => f (Proofterm.norm_proof' env der))
-                     else
-                       curry op oo (Proofterm.norm_proof' env))
-                    (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
+                   (if Envir.is_empty env then bicompose_proof
+                    else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env
+                    else Proofterm.norm_proof' env oo bicompose_proof) rder' sder,
                 {tags = [],
                  maxidx = Envir.maxidx_of env,
                  constraints = constraints',