--- 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;