# HG changeset patch
# User blanchet
# Date 1406154240 -7200
# Node ID 04ab38720b50a9cd048c6ad0297a33ea69b41d6a
# Parent  e88b5f59cadedd35b5949d69cd0429d2236cf12d
use termtab instead of (perhaps overly sensitive) thmtab

diff -r e88b5f59cade -r 04ab38720b50 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -237,8 +237,9 @@
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 
 fun substitute_noted_thm noted =
-  let val tab = fold (fold (Thmtab.default o `I) o snd) noted Thmtab.empty in
-    Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" (perhaps (Thmtab.lookup tab))
+  let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in
+    Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm"
+      (perhaps (Termtab.lookup tab o Thm.full_prop_of))
   end
 
 (* The standard binding stands for a name generated following the canonical convention (e.g.,