src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed Apr 08 19:39:08 2015 +0200
@@ -6,26 +6,26 @@
 
 signature OBJECT_LOGIC =
 sig
-  val get_base_sort: theory -> sort option
+  val get_base_sort: Proof.context -> sort option
   val add_base_sort: sort -> theory -> theory
   val add_judgment: binding * typ * mixfix -> theory -> theory
   val add_judgment_cmd: binding * string * mixfix -> theory -> theory
-  val judgment_name: theory -> string
-  val is_judgment: theory -> term -> bool
-  val drop_judgment: theory -> term -> term
-  val fixed_judgment: theory -> string -> term
-  val ensure_propT: theory -> term -> term
-  val dest_judgment: cterm -> cterm
-  val judgment_conv: conv -> conv
-  val elim_concl: thm -> term option
+  val judgment_name: Proof.context -> string
+  val is_judgment: Proof.context -> term -> bool
+  val drop_judgment: Proof.context -> term -> term
+  val fixed_judgment: Proof.context -> string -> term
+  val ensure_propT: Proof.context -> term -> term
+  val dest_judgment: Proof.context -> cterm -> cterm
+  val judgment_conv: Proof.context -> conv -> conv
+  val elim_concl: Proof.context -> thm -> term option
   val declare_atomize: attribute
   val declare_rulify: attribute
-  val atomize_term: theory -> term -> term
+  val atomize_term: Proof.context -> term -> term
   val atomize: Proof.context -> conv
   val atomize_prems: Proof.context -> conv
   val atomize_prems_tac: Proof.context -> int -> tactic
   val full_atomize_tac: Proof.context -> int -> tactic
-  val rulify_term: theory -> term -> term
+  val rulify_term: Proof.context -> term -> term
   val rulify_tac: Proof.context -> int -> tactic
   val rulify: Proof.context -> thm -> thm
   val rulify_no_asm: Proof.context -> thm -> thm
@@ -36,7 +36,7 @@
 structure Object_Logic: OBJECT_LOGIC =
 struct
 
-(** theory data **)
+(** context data **)
 
 datatype data = Data of
  {base_sort: sort option,
@@ -46,7 +46,7 @@
 fun make_data (base_sort, judgment, atomize_rulify) =
   Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
 
-structure Data = Theory_Data
+structure Data = Generic_Data
 (
   type T = data;
   val empty = make_data (NONE, NONE, ([], []));
@@ -66,7 +66,7 @@
 fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
   make_data (f (base_sort, judgment, atomize_rulify)));
 
-fun get_data thy = Data.get thy |> (fn Data args => args);
+fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args);
 
 
 
@@ -76,9 +76,10 @@
 
 val get_base_sort = #base_sort o get_data;
 
-fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
-  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
-  else (SOME S, judgment, atomize_rulify));
+fun add_base_sort S =
+  (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
+    if is_some base_sort then error "Attempt to redeclare object-logic base sort"
+    else (SOME S, judgment, atomize_rulify));
 
 
 (* add judgment *)
@@ -90,7 +91,7 @@
     thy
     |> add_consts [(b, T, mx)]
     |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
-    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
+    |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
         else (base_sort, SOME c, atomize_rulify))
   end;
@@ -105,51 +106,50 @@
 
 (* judgments *)
 
-fun judgment_name thy =
-  (case #judgment (get_data thy) of
+fun judgment_name ctxt =
+  (case #judgment (get_data ctxt) of
     SOME name => name
   | _ => raise TERM ("Unknown object-logic judgment", []));
 
-fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
+fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
   | is_judgment _ _ = false;
 
-fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
-  | drop_judgment thy (tm as (Const (c, _) $ t)) =
-      if (c = judgment_name thy handle TERM _ => false) then t else tm
+fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
+  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
+      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
   | drop_judgment _ tm = tm;
 
-fun fixed_judgment thy x =
+fun fixed_judgment ctxt x =
   let  (*be robust wrt. low-level errors*)
-    val c = judgment_name thy;
+    val c = judgment_name ctxt;
     val aT = TFree (Name.aT, []);
     val T =
-      the_default (aT --> propT) (Sign.const_type thy c)
+      the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
 
-fun ensure_propT thy t =
+fun ensure_propT ctxt t =
   let val T = Term.fastype_of t
-  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
+  in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end;
 
-fun dest_judgment ct =
-  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun dest_judgment ctxt ct =
+  if is_judgment ctxt (Thm.term_of ct)
   then Thm.dest_arg ct
   else raise CTERM ("dest_judgment", [ct]);
 
-fun judgment_conv cv ct =
-  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun judgment_conv ctxt cv ct =
+  if is_judgment ctxt (Thm.term_of ct)
   then Conv.arg_conv cv ct
   else raise CTERM ("judgment_conv", [ct]);
 
 
 (* elimination rules *)
 
-fun elim_concl rule =
+fun elim_concl ctxt rule =
   let
-    val thy = Thm.theory_of_thm rule;
     val concl = Thm.concl_of rule;
-    val C = drop_judgment thy concl;
+    val C = drop_judgment ctxt concl;
   in
     if Term.is_Var C andalso
       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
@@ -171,19 +171,19 @@
 fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
   (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
 
-val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
-val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
+val declare_atomize = Thm.declaration_attribute add_atomize;
+val declare_rulify = Thm.declaration_attribute add_rulify;
 
-val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
+val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs);
 
 
 (* atomize *)
 
-fun atomize_term thy =
-  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
+fun atomize_term ctxt =
+  drop_judgment ctxt o
+    Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
 
-fun atomize ctxt =
-  Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
+fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
 
 fun atomize_prems ctxt ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
@@ -196,11 +196,13 @@
 
 (* rulify *)
 
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
+fun rulify_term ctxt =
+  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) [];
+
+fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
 
 fun gen_rulify full ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
+  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
   #> Drule.gen_all (Variable.maxidx_of ctxt)
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;