# HG changeset patch
# User haftmann
# Date 1156150962 -7200
# Node ID 14d5f6ed5602b3cd940ecb69086720bfc71d4c69
# Parent  e2c6d096af01d3666883106bb8b72b9aa1be6808
fixed bug in sortlookup

diff -r e2c6d096af01 -r 14d5f6ed5602 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Aug 21 11:02:41 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon Aug 21 11:02:42 2006 +0200
@@ -601,8 +601,8 @@
     fun constructor tyco lss class =
       Instance ((class, tyco), (map o map) fst lss);
     fun variable (TFree (v, sort)) =
-          map_index (fn (n, class) => (Lookup ([], (v, (n, length sort))), class))
-            (operational_sort_of thy sort);
+      let val op_sort = operational_sort_of thy sort
+      in map_index (fn (n, class) => (Lookup ([], (v, (n, length op_sort))), class)) op_sort end;
   in
     Sorts.of_sort_derivation pp algebra
       {classrel = classrel, constructor = constructor, variable = variable}