# HG changeset patch
# User wenzelm
# Date 976561871 -3600
# Node ID 66d093e2076ec6398b5306f63b59d9b995689c6d
# Parent  5be46cd1f94a28032ff7de1a48195aa0ed528573
moved "_update_name" to HOL/Record;

diff -r 5be46cd1f94a -r 66d093e2076e src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Dec 11 20:10:42 2000 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Dec 11 20:11:11 2000 +0100
@@ -217,7 +217,6 @@
 *}
 
 syntax
-  "_update_name" :: idt
   "_quote"       :: "'b => ('a => 'b)"        ("(.'(_').)" [0] 1000)
   "_antiquote"   :: "('a => 'b) => 'b"        ("`_" [1000] 1000)
   "_Assert"      :: "'a => 'a set"            ("(.{_}.)" [0] 1000)
@@ -241,19 +240,9 @@
 
 parse_translation {*
   let
-    fun update_name_tr (Free (x, T) :: ts) =
-          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
-      | update_name_tr (Const (x, T) :: ts) =
-          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
-      | update_name_tr
-          (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-            Term.list_comb (c $ update_name_tr [t] $
-              (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
-      | update_name_tr ts = raise TERM ("update_name_tr", ts);
-
     fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
       | quote_tr ts = raise TERM ("quote_tr", ts);
-  in [("_update_name", update_name_tr), ("_quote", quote_tr)] end
+  in [("_quote", quote_tr)] end
 *}
 
 text {*