tuned whitespace;
authorwenzelm
Thu, 10 Oct 2019 14:55:26 +0200
changeset 71013 c6f2a73987cd
parent 71012 22e2f5acc0b4
child 71014 7000868c6098
tuned whitespace;
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)