src/Pure/Isar/code_unit.ML

   val error_thm: (thm -> thm) -> thm -> thm
   val warning_thm: (thm -> thm) -> thm -> thm option
   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
 
   (*constants*)
   val add_const_ident: thm -> theory -> theory

     val c' :: cs' = map ty_sorts cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
     val vs = Name.names Name.context Name.aT sorts;
     val cs''' = map (inst vs) cs'';
   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 =