src/Pure/axclass.ML
changeset 62897 8093203f0b89
parent 61262 7bd1eb4b056e
child 63073 413184c7a2a2
--- a/src/Pure/axclass.ML	Thu Apr 07 11:17:57 2016 +0200
+++ b/src/Pure/axclass.ML	Thu Apr 07 12:08:02 2016 +0200
@@ -261,12 +261,13 @@
     else SOME (map_proven_arities (K arities') thy)
   end;
 
-val _ = Theory.setup
-  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
-
-val _ = Proofterm.install_axclass_proofs
-  {classrel_proof = Thm.proof_of oo the_classrel,
-   arity_proof = Thm.proof_of oo the_arity};
+val _ =
+  Theory.setup
+   (Theory.at_begin complete_classrels #>
+    Theory.at_begin complete_arities #>
+    Proofterm.install_axclass_proofs
+     {classrel_proof = Thm.proof_of oo the_classrel,
+      arity_proof = Thm.proof_of oo the_arity});
 
 
 (* maintain instance parameters *)