# HG changeset patch
# User wenzelm
# Date 1301428081 -7200
# Node ID fa108629d13294ab16218592fb7e9a01320a685f
# Parent  6c17259724b2735ceb293f0347b1691dc38b65a5
use shared copy of hoare_syntax.ML;
misc tuning;

diff -r 6c17259724b2 -r fa108629d132 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 29 21:48:01 2011 +0200
@@ -10,7 +10,7 @@
 
 theory Hoare_Logic
 imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
 types
@@ -45,9 +45,6 @@
   where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
 
 
-
-(** parse translations **)
-
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
@@ -58,126 +55,10 @@
  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
-parse_translation {*
-  let
-    fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
-      | mk_abstuple (x :: xs) body =
-          Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
-
-    fun mk_fbody x e [y] = if Syntax.eq_idt (x, y) then e else y
-      | mk_fbody x e (y :: xs) =
-          Syntax.const @{const_syntax Pair} $
-            (if Syntax.eq_idt (x, y) then e else y) $ mk_fbody x e xs;
-
-    fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
-
-    (* bexp_tr & assn_tr *)
-    (*all meta-variables for bexp except for TRUE are translated as if they
-      were boolean expressions*)
-
-    fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
-      | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-    fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-
-    (* com_tr *)
-
-    fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
-          Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
-      | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
-      | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
-          Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
-      | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
-          Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-      | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
-          Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
-      | com_tr t _ = t;
-
-    fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
-      | vars_tr t = [t];
-
-    fun hoare_vars_tr [vars, pre, prg, post] =
-          let val xs = vars_tr vars
-          in Syntax.const @{const_syntax Valid} $
-             assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
-          end
-      | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-
-  in [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] end
-*}
-
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
-                            subst_bound (Syntax.free v, dest_abstuple body)
-  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
-  | dest_abstuple trm = trm;
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
 
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
-  | abs2list (Abs(x,T,t)) = [Free (x, T)]
-  | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
-  | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
-  | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
-           ((Syntax.free x)::(abs2list t), mk_ts t)
-  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
-  | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
-  | find_ch ((v,t)::vts) i xs =
-      if t = Bound i then find_ch vts (i-1) xs
-      else (true, (v, subst_bounds (xs, t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
-  | is_f (Abs(x,_,t)) = true
-  | is_f t = false;
-*}
-
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_syntax inter}, _) $
-        (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
-      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
-  | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
-  let val (vs, ts) = mk_vts f;
-      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in
-    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
-    else Syntax.const @{const_syntax annskip}
-  end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
-      if is_f f then mk_assign f
-      else Syntax.const @{const_syntax Basic} $ f
-  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
-      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
-      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
-      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
-  | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
-  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
diff -r 6c17259724b2 -r fa108629d132 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue Mar 29 21:48:01 2011 +0200
@@ -7,7 +7,7 @@
 
 theory Hoare_Logic_Abort
 imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
 types
@@ -47,9 +47,6 @@
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
 
 
-
-(** parse translations **)
-
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
@@ -60,126 +57,11 @@
   "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
-parse_translation {*
-  let
-    fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
-      | mk_abstuple (x :: xs) body =
-          Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
-
-    fun mk_fbody x e [y] = if Syntax.eq_idt (x, y) then e else y
-      | mk_fbody x e (y :: xs) =
-          Syntax.const @{const_syntax Pair} $
-            (if Syntax.eq_idt (x, y) then e else y) $ mk_fbody x e xs;
-
-    fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
-
-    (* bexp_tr & assn_tr *)
-    (*all meta-variables for bexp except for TRUE are translated as if they
-      were boolean expressions*)
-
-    fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
-      | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-    fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-
-    (* com_tr *)
-
-    fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
-          Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
-      | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
-      | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
-          Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
-      | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
-          Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-      | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
-          Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
-      | com_tr t _ = t;
-
-    fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
-      | vars_tr t = [t];
-
-    fun hoare_vars_tr [vars, pre, prg, post] =
-          let val xs = vars_tr vars
-          in Syntax.const @{const_syntax Valid} $
-             assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
-          end
-      | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-
-  in [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] end
-*}
-
-
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
-      subst_bound (Syntax.free v, dest_abstuple body)
-  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
-  | dest_abstuple trm = trm;
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation
+  {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
 
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
-  | abs2list (Abs(x,T,t)) = [Free (x, T)]
-  | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
-  | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
-  | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
-           ((Syntax.free x)::(abs2list t), mk_ts t)
-  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
-  | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
-  | find_ch ((v,t)::vts) i xs =
-      if t = Bound i then find_ch vts (i-1) xs
-      else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
-  | is_f (Abs(x,_,t)) = true
-  | is_f t = false;
-*}
-
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
-        (Const (@{const_syntax Collect},_) $ T2)) =
-      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
-  | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
-  let val (vs, ts) = mk_vts f;
-      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in
-    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
-    else Syntax.const @{const_syntax annskip}
-  end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
-      if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
-  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
-      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
-      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
-      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
-  | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
-  Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 (*** The proof rules ***)
 
diff -r 6c17259724b2 -r fa108629d132 src/HOL/Hoare/hoare_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML	Tue Mar 29 21:48:01 2011 +0200
@@ -0,0 +1,156 @@
+(*  Title:      HOL/Hoare/hoare_syntax.ML
+    Author:     Leonor Prensa Nieto & Tobias Nipkow
+
+Syntax translations for Hoare logic.
+*)
+
+signature HOARE_SYNTAX =
+sig
+  val hoare_vars_tr: term list -> term
+  val spec_tr': string -> term list -> term
+end;
+
+structure Hoare_Syntax: HOARE_SYNTAX =
+struct
+
+(** parse translation **)
+
+local
+
+fun idt_name (Free (x, _)) = SOME x
+  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
+  | idt_name _ = NONE;
+
+fun eq_idt tu =
+  (case pairself idt_name tu of
+    (SOME x, SOME y) => x = y
+  | _ => false);
+
+fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
+  | mk_abstuple (x :: xs) body =
+      Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
+
+fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
+  | mk_fbody x e (y :: xs) =
+      Syntax.const @{const_syntax Pair} $
+        (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
+
+fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
+
+
+(* bexp_tr & assn_tr *)
+(*all meta-variables for bexp except for TRUE are translated as if they
+  were boolean expressions*)
+
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
+  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
+
+
+(* com_tr *)
+
+fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
+      Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
+  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+  | com_tr t _ = t;
+
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
+  | vars_tr t = [t];
+
+in
+
+fun hoare_vars_tr [vars, pre, prg, post] =
+      let val xs = vars_tr vars
+      in Syntax.const @{const_syntax Valid} $
+         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+      end
+  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+
+end;
+
+
+
+(** print translation **)
+
+local
+
+fun dest_abstuple
+      (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
+        subst_bound (Syntax.free v, dest_abstuple body)
+  | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
+  | dest_abstuple tm = tm;
+
+fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+  | abs2list (Abs (x, T, t)) = [Free (x, T)]
+  | abs2list _ = [];
+
+fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
+  | mk_ts (Abs (x, _, t)) = mk_ts t
+  | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
+  | mk_ts t = [t];
+
+fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
+      (Syntax.free x :: abs2list t, mk_ts t)
+  | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
+  | mk_vts t = raise Match;
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
+  | find_ch ((v, t) :: vts) i xs =
+      if t = Bound i then find_ch vts (i - 1) xs
+      else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
+  | is_f (Abs (x, _, t)) = true
+  | is_f t = false;
+
+
+(* assn_tr' & bexp_tr'*)
+
+fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+  | assn_tr' (Const (@{const_syntax inter}, _) $
+        (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
+      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
+  | assn_tr' t = t;
+
+fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+  | bexp_tr' t = t;
+
+
+(* com_tr' *)
+
+fun mk_assign f =
+  let
+    val (vs, ts) = mk_vts f;
+    val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+  in
+    if ch
+    then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+    else Syntax.const @{const_syntax annskip}
+  end;
+
+fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
+      if is_f f then mk_assign f
+      else Syntax.const @{const_syntax Basic} $ f
+  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
+      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
+      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
+  | com_tr' t = t;
+
+in
+
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+
+end;
+
+end;
+
diff -r 6c17259724b2 -r fa108629d132 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Mar 29 21:48:01 2011 +0200
@@ -650,12 +650,12 @@
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
-  Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy			\
-  Hoare/Hoare_Logic.thy	Hoare/Hoare_Logic_Abort.thy			\
+  Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML		\
+  Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy	\
   Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
   Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
-  Hoare/SchorrWaite.thy Hoare/Separation.thy				\
-  Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
+  Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy	\
+  Hoare/document/root.tex Hoare/document/root.bib
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
 
 
diff -r 6c17259724b2 -r fa108629d132 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 29 21:11:02 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 29 21:48:01 2011 +0200
@@ -37,7 +37,6 @@
   val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
   val constrainAbsC: string
   val abs_tr: term list -> term
-  val eq_idt: term * term -> bool
   val pure_trfuns:
     (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
@@ -116,18 +115,6 @@
   | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
-(* equality on idt *)
-
-fun idt_name (Free (x, _)) = SOME x
-  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
-  | idt_name _ = NONE;
-
-fun eq_idt tu =
-  (case pairself idt_name tu of
-    (SOME x, SOME y) => x = y
-  | _ => false);
-
-
 (* binder *)
 
 fun mk_binder_tr (syn, name) =