# HG changeset patch
# User wenzelm
# Date 1003082959 -7200
# Node ID fd780dd6e0b4b00032f281a0e2788a0c24f03a5c
# Parent  41ae2eb50bbfe09cdc6cec1b0e10ea1524a5611c
use ObjectLogic;

diff -r 41ae2eb50bbf -r fd780dd6e0b4 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Sun Oct 14 20:09:19 2001 +0200
@@ -11,78 +11,41 @@
 
 signature AUTO_BIND =
 sig
-  val is_judgment: term -> bool
-  val drop_judgment: term -> term
-  val atomic_judgment: theory -> string -> term
-  val add_judgment: bstring * string * mixfix -> theory -> theory
-  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
-  val goal: term -> (indexname * term option) list
-  val facts: string -> term list -> (indexname * term option) list
+  val goal: Sign.sg -> term -> (indexname * term option) list
+  val facts: Sign.sg -> string -> term list -> (indexname * term option) list
   val thesisN: string
 end;
 
 structure AutoBind: AUTO_BIND =
 struct
 
-
-(** judgments **)
-
-val TruepropN = "Trueprop";
-
-fun is_judgment (Const (c, _) $ _) = c = TruepropN
-  | is_judgment _ = false;
-
-fun drop_judgment (Abs (x, T, t)) = Abs (x, T, drop_judgment t)
-  | drop_judgment (tm as (Const (c, _) $ t)) = if c = TruepropN then t else tm
-  | drop_judgment tm = tm;
-
-val strip_judgment = drop_judgment o Logic.strip_assums_concl;
-
-fun atomic_judgment thy x =
-  let  (*be robust wrt. low-level errors*)
-    val aT = TFree ("'a", logicS);
-    val T =
-      if_none (Sign.const_type (Theory.sign_of thy) TruepropN) (aT --> propT)
-      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
-    val U = Term.domain_type T handle Match => aT;
-  in Const (TruepropN, T) $ Free (x, U) end;
-
-
-fun gen_add_judgment add (name, T, syn) thy =
-  if name = TruepropN then
-    thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path
-  else error ("Judgment name has to be " ^ quote TruepropN);
-
-val add_judgment = gen_add_judgment Theory.add_consts;
-val add_judgment_i = gen_add_judgment Theory.add_consts_i;
-
-
-
 (** bindings **)
 
 val thesisN = "thesis";
 val thisN = "this";
 
-fun statement_binds name prop =
-  [((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment prop)))];
+fun strip_judgment sg = ObjectLogic.drop_judgment sg o Logic.strip_assums_concl;
+
+fun statement_binds sg name prop =
+  [((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment sg prop)))];
 
 
 (* goal *)
 
-fun goal prop = statement_binds thesisN prop;
+fun goal sg prop = statement_binds sg thesisN prop;
 
 
 (* facts *)
 
-fun get_arg prop =
-  (case strip_judgment prop of
+fun get_arg sg prop =
+  (case strip_judgment sg prop of
     _ $ t => Some (Term.list_abs (Logic.strip_params prop, t))
   | _ => None);
 
-fun facts _ [] = []
-  | facts name props =
+fun facts _ _ [] = []
+  | facts sg name props =
       let val prop = Library.last_elem props
-      in [(Syntax.dddot_indexname, get_arg prop)] @ statement_binds thisN prop end;
+      in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end;
 
 
 end;
diff -r 41ae2eb50bbf -r fd780dd6e0b4 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun Oct 14 20:09:19 2001 +0200
@@ -251,8 +251,8 @@
 fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
 val add_trrules = Theory.add_trrules o map Comment.ignore;
 val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
-val add_judgment = AutoBind.add_judgment o Comment.ignore;
-val add_judgment_i = AutoBind.add_judgment_i o Comment.ignore;
+val add_judgment = ObjectLogic.add_judgment o Comment.ignore;
+val add_judgment_i = ObjectLogic.add_judgment_i o Comment.ignore;
 
 
 (* axioms and defs *)
diff -r 41ae2eb50bbf -r fd780dd6e0b4 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Oct 14 20:09:19 2001 +0200
@@ -51,7 +51,7 @@
     if not (null bads) then
       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
         space_implode " " (map (Sign.string_of_term sign) bads), state)
-    else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
+    else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
   end;
@@ -67,6 +67,7 @@
     val _ = Proof.assert_forward_or_chain state;
     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
     val thy = Proof.theory_of state;
+    val sign = Theory.sign_of thy;
 
     (*obtain vars*)
     val (vars_ctxt, vars) =
@@ -86,7 +87,7 @@
     (*that_prop*)
     val thesisN = Term.variant xs AutoBind.thesisN;
     val bound_thesis =
-      ProofContext.bind_skolem fix_ctxt [thesisN] (AutoBind.atomic_judgment thy thesisN);
+      ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
 
     fun occs_var x = Library.get_first (fn t =>
       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
diff -r 41ae2eb50bbf -r fd780dd6e0b4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 14 20:09:19 2001 +0200
@@ -693,8 +693,11 @@
 val add_binds = gen_binds read_term;
 val add_binds_i = gen_binds cert_term;
 
-val auto_bind_goal = add_binds_i o map drop_schematic o AutoBind.goal;
-val auto_bind_facts = (add_binds_i o map drop_schematic) oo AutoBind.facts;
+fun auto_bind_goal t ctxt =
+  ctxt |> add_binds_i (map drop_schematic (AutoBind.goal (sign_of ctxt) t));
+
+fun auto_bind_facts name ts ctxt =
+  ctxt |> add_binds_i (map drop_schematic (AutoBind.facts (sign_of ctxt) name ts));
 
 end;
 
diff -r 41ae2eb50bbf -r fd780dd6e0b4 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Sun Oct 14 20:09:19 2001 +0200
@@ -85,7 +85,8 @@
     val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
     val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
-    val bind = ((case_conclN, 0), Some (if raw then concl else AutoBind.drop_judgment concl));
+    val bind = ((case_conclN, 0),
+      Some (if raw then concl else ObjectLogic.drop_judgment (Thm.sign_of_thm thm) concl));
   in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
 
 fun gen_make raw open_parms raw_thm names =