# HG changeset patch
# User wenzelm
# Date 1570712126 -7200
# Node ID c6f2a73987cdf7f05ec0edccf4d2c0332c8cbeba
# Parent  22e2f5acc0b4439835537b17beaa2fae56f34f09
tuned whitespace;

diff -r 22e2f5acc0b4 -r c6f2a73987cd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 10 14:53:48 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 10 14:55:26 2019 +0200
@@ -2065,7 +2065,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)