# HG changeset patch
# User wenzelm
# Date 1288383756 -7200
# Node ID 80136c4240cc835257c40eb859a0aea50d9dea9c
# Parent  c9acf88447e6970b9544ab8cd8eec6bcdfce3bed
simplified data lookup;

diff -r c9acf88447e6 -r 80136c4240cc src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Oct 29 22:19:27 2010 +0200
+++ b/src/Tools/subtyping.ML	Fri Oct 29 22:22:36 2010 +0200
@@ -63,7 +63,7 @@
   map_data (fn (coes, coes_graph, tmaps) =>
     (coes, coes_graph, f tmaps));
 
-fun rep_data context = Data.get context |> (fn Data args => args);
+val rep_data = (fn Data args => args) o Data.get o Context.Proof;
 
 val coes_of = #coes o rep_data;
 val coes_graph_of = #coes_graph o rep_data;
@@ -275,8 +275,8 @@
 
 fun process_constraints ctxt cs tye_idx =
   let
-    val coes_graph = coes_graph_of (Context.Proof ctxt);
-    val tmaps = tmaps_of (Context.Proof ctxt);
+    val coes_graph = coes_graph_of ctxt;
+    val tmaps = tmaps_of ctxt;
     val tsig = Sign.tsig_of (ProofContext.theory_of ctxt);
     val pp = Syntax.pp ctxt;
     val arity_sorts = Type.arity_sorts pp tsig;
@@ -556,7 +556,7 @@
           if a = b
           then Abs (Name.uu, Type (a, []), Bound 0)
           else
-            (case Symreltab.lookup (coes_of (Context.Proof ctxt)) (a, b) of
+            (case Symreltab.lookup (coes_of ctxt) (a, b) of
               NONE => raise Fail (a ^ " is not a subtype of " ^ b)
             | SOME co => co)
       | gen_coercion ((Type (a, Ts)), (Type (b, Us))) =
@@ -572,7 +572,7 @@
               fun ts_of [] = []
                 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
             in
-              (case Symtab.lookup (tmaps_of (Context.Proof ctxt)) a of
+              (case Symtab.lookup (tmaps_of ctxt) a of
                 NONE => raise Fail ("No map function for " ^ a ^ " known")
               | SOME tmap =>
                   let