# HG changeset patch
# User wenzelm
# Date 877353489 -7200
# Node ID 9666a1ecf3a14583fe96e9e3462c0a30d8aabf7f
# Parent  c8c188655948b2b8f7dd74e4da0599a45e5e3d3f
tuned sig;

diff -r c8c188655948 -r 9666a1ecf3a1 src/HOL/typedef.ML
--- 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;