# HG changeset patch
# User haftmann
# Date 1177084705 -7200
# Node ID e4a3f49eb924c008bbcbae741c75af667ac56dff
# Parent  a7790c8e3c14a5e777ed4b7615a6f03cbce42b58
reverted to classical syntax for K_record

diff -r a7790c8e3c14 -r e4a3f49eb924 src/HOL/HoareParallel/OG_Syntax.thy
--- a/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 17:58:24 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 17:58:25 2007 +0200
@@ -10,8 +10,8 @@
   "_AnnAssign"   :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
-  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
+  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
+  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
 
 syntax
   "_AnnSkip"     :: "'a assn \<Rightarrow> 'a ann_com"              ("_//SKIP" [90] 63)
diff -r a7790c8e3c14 -r e4a3f49eb924 src/HOL/HoareParallel/RG_Syntax.thy
--- a/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:24 2007 +0200
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:25 2007 +0200
@@ -16,7 +16,7 @@
   "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
+  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
   "SKIP" \<rightleftharpoons> "Basic id"
   "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
@@ -78,7 +78,7 @@
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
 
-    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
+    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"}, _)$t) $ Bound 0) :: ts) =
           quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
             (Abs (x, dummyT, t) :: ts)
       | assign_tr' _ = raise Match;
diff -r a7790c8e3c14 -r e4a3f49eb924 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:24 2007 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:25 2007 +0200
@@ -228,8 +228,8 @@
 
 translations
   ".{b}."                   => "Collect .(b)."
-  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (CONST K_record a)) \<in> B}."
-  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (CONST K_record a)))."
+  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
+  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (K_record a)))."
   "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
   "WHILE b INV i DO c OD"   => "While .{b}. i c"
   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
@@ -270,7 +270,7 @@
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
 
-    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
+    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
           quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
             (Abs (x, dummyT, t) :: ts)
       | assign_tr' _ = raise Match;
@@ -448,7 +448,7 @@
 method_setup hoare = {*
   Method.no_args
     (Method.SIMPLE_METHOD'
-       (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *}
+       (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_apply"}] )))) *}
   "verification condition generator for Hoare logic"
 
 end
diff -r a7790c8e3c14 -r e4a3f49eb924 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Apr 20 17:58:24 2007 +0200
+++ b/src/HOL/Record.thy	Fri Apr 20 17:58:25 2007 +0200
@@ -17,10 +17,9 @@
 lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   by simp
 
-definition
+constdefs
   K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
-where
-  K_record_apply [simp]: "K_record c x = c"
+  K_record_apply [simp, code func]: "K_record c x \<equiv> c"
 
 lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
   by (rule ext) (simp add: K_record_apply comp_def)