# HG changeset patch
# User haftmann
# Date 1245613567 -7200
# Node ID 75fe3304015c0bf6baf4f001c5b10d4100b1a8bb
# Parent  dc3c2d52b642a16269526f3fbeaa6b622da20f48
code equation observes default sort constraints for types

diff -r dc3c2d52b642 -r 75fe3304015c src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Sun Jun 21 21:37:24 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Sun Jun 21 21:46:07 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;