tuned sig;

--- a/src/HOL/typedef.ML	Mon Oct 20 12:50:18 1997 +0200
+++ b/src/HOL/typedef.ML	Mon Oct 20 15:18:09 1997 +0200
@@ -8,9 +8,9 @@
 signature TYPEDEF =
 sig
   val prove_nonempty: cterm -> thm list -> tactic option -> thm
-  val add_typedef: string -> rstring * string list * mixfix ->
+  val add_typedef: string -> bstring * string list * mixfix ->
     string -> string list -> thm list -> tactic option -> theory -> theory
-  val add_typedef_i: string -> rstring * string list * mixfix ->
+  val add_typedef_i: string -> bstring * string list * mixfix ->
     term -> string list -> thm list -> tactic option -> theory -> theory
 end;
 
@@ -127,12 +127,12 @@
 
 (* external interfaces *)
 
+fun read_term sg str =
+  read_cterm sg (str, HOLogic.termTVar);
+
 fun cert_term sg tm =
   cterm_of sg tm handle TERM (msg, _) => error msg;
 
-fun read_term sg str =
-  read_cterm sg (str, HOLogic.termTVar);
-
 val add_typedef = ext_typedef read_term;
 val add_typedef_i = ext_typedef cert_term;