removed dead code;
authorwenzelm
Tue, 13 Dec 2011 20:10:28 +0100
changeset 45836 8bed07ec172b
parent 45835 14bf7ca4ef3a
child 45837 086ff24a9aa3
removed dead code;
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;