--- a/src/Tools/Code/code_ml.ML Thu Jun 17 10:45:10 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jun 17 10:51:38 2010 +0200
@@ -32,7 +32,7 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * ((class * (string * (vname * sort) list))
- * (((class * (string * (string * dict list list))) list * (class * class) list list)
+ * ((class * (string * (string * dict list list))) list
* ((string * const) * (thm * bool)) list));
datatype ml_stmt =
@@ -219,7 +219,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [
@@ -554,7 +554,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [