--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 19:41:19 2010 +0200
@@ -15,10 +15,10 @@
datatype arLit =
TConsLit of name * name * name list |
TVarLit of name * name
- datatype arity_clause = ArityClause of
- {axiom_name: string, conclLit: arLit, premLits: arLit list}
- datatype class_rel_clause = ClassRelClause of
- {axiom_name: string, subclass: name, superclass: name}
+ datatype arity_clause =
+ ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ datatype class_rel_clause =
+ ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
datatype combtyp =
CombTVar of name |
CombTFree of name |