# HG changeset patch
# User wenzelm
# Date 1323803428 -3600
# Node ID 8bed07ec172b31ad5bb4f72d5d489fa0c0ee0dae
# Parent  14bf7ca4ef3a1b34c50ff998e4e4cfd2825d2477
removed dead code;

diff -r 14bf7ca4ef3a -r 8bed07ec172b src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Dec 13 20:10:11 2011 +0100
+++ b/src/HOL/Tools/record.ML	Tue Dec 13 20:10:28 2011 +0100
@@ -49,8 +49,6 @@
   val updateN: string
   val ext_typeN: string
   val extN: string
-  val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
-  val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
   val setup: theory -> theory
 end;
 
@@ -1489,24 +1487,6 @@
 
 (** theory extender interface **)
 
-(* prepare arguments *)
-
-fun read_typ ctxt raw_T env =
-  let
-    val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
-    val T = Syntax.read_typ ctxt' raw_T;
-    val env' = Term.add_tfreesT T env;
-  in (T, env') end;
-
-fun cert_typ ctxt raw_T env =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val T = Type.no_tvars (Sign.certify_typ thy raw_T)
-      handle TYPE (msg, _, _) => error msg;
-    val env' = Term.add_tfreesT T env;
-  in (T, env') end;
-
-
 (* attributes *)
 
 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;