records without signature
authornarasche
Fri, 19 Dec 1997 13:31:08 +0100
changeset 4459 4066db36616b
parent 4458 ad8be126603d
child 4460 8b9647d5b632
records without signature
src/HOL/record.ML
--- a/src/HOL/record.ML	Fri Dec 19 13:30:21 1997 +0100
+++ b/src/HOL/record.ML	Fri Dec 19 13:31:08 1997 +0100
@@ -209,8 +209,7 @@
      in 
        case opt_info of 
          None => ["Parent " ^ quote parent ^" not defined"]
-       | Some {args = pargs, parent = pparent, 
-               fields = pfields, sign_ref = psign_ref} =>
+       | Some {args = pargs, parent = pparent, fields = pfields} =>
            if (length args = length pargs) 
              then check_sorts pargs args
              else ["Mismatching arities for parent " ^ quote (base parent)] 
@@ -256,8 +255,7 @@
     val full = Sign.full_name sign;
 
     val current_fullfields = map (apfst full) current_fields;
-    val info = {args = args, fields = current_fullfields, 
-                    parent = opt_parent, sign_ref = Sign.self_ref sign};
+    val info = {args = args, fields = current_fullfields, parent = opt_parent};
     val thy = thy |> put_record thy full_name info;
     val all_types = record_field_types thy info; 
     val all_fields = record_field_names thy info ~~ all_types;