# HG changeset patch
# User wenzelm
# Date 964954293 -7200
# Node ID e290583864e45e1095ca4c3d311f2ce0293080eb
# Parent  4362bf779182ae14e288d0ab4326dde454d24152
added is_judgment;
removed atomic_thesis;

diff -r 4362bf779182 -r e290583864e4 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sun Jul 30 12:50:51 2000 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Sun Jul 30 12:51:33 2000 +0200
@@ -14,7 +14,7 @@
   val goal: term -> (indexname * term option) list
   val facts: string -> term list -> (indexname * term option) list
   val thesisN: string
-  val atomic_thesis: term -> term * term
+  val is_judgment: term -> bool
   val add_judgment: bstring * string * mixfix -> theory -> theory
   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
 end;
@@ -58,17 +58,17 @@
       in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end;
 
 
-(* atomic_thesis *)
+
+(** judgments **)
 
-fun mk_free t = Free (thesisN, Term.fastype_of t);
-
-fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = (t, c $ mk_free t)
-  | atomic_thesis t = (t, mk_free t);
+fun is_judgment (Const ("Trueprop", _) $ _) = true
+  | is_judgment _ = false;
 
 
-(** judgment **)
-
-fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
+fun gen_add_judgment add (name, T, syn) thy =
+  if name = "Trueprop" then
+    thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path
+  else error "Judgment name has to be \"Trueprop\"";
 
 val add_judgment = gen_add_judgment Theory.add_consts;
 val add_judgment_i = gen_add_judgment Theory.add_consts_i;