# HG changeset patch
# User narasche
# Date 882534668 -3600
# Node ID 4066db36616bf157333965b3dece30a4c6884e19
# Parent  ad8be126603d484a0243c9d2c719a1f00201bec9
records without signature

diff -r ad8be126603d -r 4066db36616b 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;