# HG changeset patch
# User wenzelm
# Date 1322665515 -3600
# Node ID bbd2c7ffc02c28ec14841ecaea510709167cbd7f
# Parent  d2567e55af83db8ebcef025f8d54334e332a9bd8
tuned layout;

diff -r d2567e55af83 -r bbd2c7ffc02c src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed Nov 30 16:03:18 2011 +0100
+++ b/src/HOL/Typerep.thy	Wed Nov 30 16:05:15 2011 +0100
@@ -63,8 +63,9 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
-fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
-  andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
+fun ensure_typerep tyco thy =
+  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
+    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
   then add_typerep tyco thy else thy;
 
 in