--- 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;