# HG changeset patch
# User haftmann
# Date 1245651472 -7200
# Node ID 8361d7a517b444834fef7e174836c9c9d0daae4e
# Parent  c494ae8970e14123987b68fbc91d11134051be5b# Parent  75fe3304015c0bf6baf4f001c5b10d4100b1a8bb
merged

diff -r c494ae8970e1 -r 8361d7a517b4 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Mon Jun 22 08:00:46 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Mon Jun 22 08:17:52 2009 +0200
@@ -85,7 +85,9 @@
     end;
   fun add_term_of_code tyco raw_vs raw_cs thy =
     let
-      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+      val algebra = Sign.classes_of thy;
+      val vs = map (fn (v, sort) =>
+        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
       val ty = Type (tyco, map TFree vs);
       val cs = (map o apsnd o map o map_atyps)
         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;