# HG changeset patch
# User haftmann
# Date 1155017951 -7200
# Node ID 54fe257afd4fd550872adeba7dc34227f9a9bb22
# Parent  1bf581bc4d60c90e8a634fc58922ea178cd83dc7
dropped duplicated line

diff -r 1bf581bc4d60 -r 54fe257afd4f src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Aug 08 08:19:06 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Aug 08 08:19:11 2006 +0200
@@ -69,7 +69,6 @@
 val ext_dest = "_sel";
 val updateN = "_update";
 val updN = "_upd";
-val schemeN = "_scheme";
 val makeN = "make";
 val fields_selN = "fields";
 val extendN = "extend";