# HG changeset patch
# User wenzelm
# Date 963481266 -7200
# Node ID 0d2b31e1ea1b910fa24191933f1b478a9476da88
# Parent  5fc3c1f84e8a7f7022e40000d4713ce052150c7a
export thesisN separately;

diff -r 5fc3c1f84e8a -r 0d2b31e1ea1b src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Thu Jul 13 11:40:49 2000 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Thu Jul 13 11:41:06 2000 +0200
@@ -13,7 +13,8 @@
 sig
   val goal: term -> (indexname * term option) list
   val facts: string -> term list -> (indexname * term option) list
-  val atomic_thesis: term -> (string * term) * term
+  val thesisN: string
+  val atomic_thesis: term -> term * term
   val add_judgment: bstring * string * mixfix -> theory -> theory
   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
 end;
@@ -61,8 +62,8 @@
 
 fun mk_free t = Free (thesisN, Term.fastype_of t);
 
-fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
-  | atomic_thesis t = ((thesisN, t), mk_free t);
+fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = (t, c $ mk_free t)
+  | atomic_thesis t = (t, mk_free t);
 
 
 (** judgment **)