# HG changeset patch
# User haftmann
# Date 1205907634 -3600
# Node ID e493bdd1cff2aa63cff34235348b7091b864ac1b
# Parent  3e58e4c67a2a9caf159a3bd270477ebcc2d845f5
moved typ_of_inst to Type.typ_of_sort

diff -r 3e58e4c67a2a -r e493bdd1cff2 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Wed Mar 19 07:20:33 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML	Wed Mar 19 07:20:34 2008 +0100
@@ -14,8 +14,6 @@
   val try_thm: (thm -> thm) -> thm -> thm option
 
   (*typ instantiations*)
-  val typ_sort_inst: Sorts.algebra -> typ * sort
-    -> sort Vartab.table -> sort Vartab.table
   val inst_thm: sort Vartab.table -> thm -> thm
   val constrain_thm: sort -> thm -> thm
 
@@ -148,18 +146,6 @@
   in (tyco, (vs, cs''')) end;
 
 
-(* dictionary values *)
-
-fun typ_sort_inst algebra =
-  let
-    val inters = Sorts.inter_sort algebra;
-    fun match _ [] = I
-      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
-      | match (Type (a, Ts)) S =
-          fold2 match Ts (Sorts.mg_domain algebra a S)
-  in uncurry match end;
-
-
 (* rewrite theorems *)
 
 fun assert_rew thm =