# 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)