misc tuning and clarification, notably wrt. flow of context;
authorwenzelm
Tue Jun 04 13:14:17 2019 +0200 (6 weeks ago)
changeset 70316c61b7af108a6
parent 70315 2f9623aa1eeb
child 70317 9fced5690f4e
misc tuning and clarification, notably wrt. flow of context;
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
     1.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Tue Jun 04 13:09:24 2019 +0200
     1.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Jun 04 13:14:17 2019 +0200
     1.3 @@ -124,36 +124,27 @@
     1.4        pred_data = Symtab.merge (K true) (pd1, pd2) }
     1.5  )
     1.6  
     1.7 -fun get_transfer_raw ctxt = ctxt
     1.8 -  |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
     1.9 +val get_transfer_raw = Item_Net.content o #transfer_raw o Data.get o Context.Proof
    1.10  
    1.11 -fun get_known_frees ctxt = ctxt
    1.12 -  |> (#known_frees o Data.get o Context.Proof)
    1.13 +val get_known_frees = #known_frees o Data.get o Context.Proof
    1.14  
    1.15 -fun get_compound_lhs ctxt = ctxt
    1.16 -  |> (#compound_lhs o Data.get o Context.Proof)
    1.17 +val get_compound_lhs = #compound_lhs o Data.get o Context.Proof
    1.18  
    1.19 -fun get_compound_rhs ctxt = ctxt
    1.20 -  |> (#compound_rhs o Data.get o Context.Proof)
    1.21 +val get_compound_rhs = #compound_rhs o Data.get o Context.Proof
    1.22  
    1.23 -fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
    1.24 +val get_relator_eq_item_net = #relator_eq o Data.get o Context.Proof
    1.25  
    1.26 -fun get_relator_eq ctxt = ctxt
    1.27 -  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
    1.28 -  |> map safe_mk_meta_eq
    1.29 +val get_relator_eq =
    1.30 +  map safe_mk_meta_eq o Item_Net.content o #relator_eq o Data.get o Context.Proof
    1.31  
    1.32 -fun get_sym_relator_eq ctxt = ctxt
    1.33 -  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
    1.34 -  |> map (Thm.symmetric o safe_mk_meta_eq)
    1.35 +val get_sym_relator_eq =
    1.36 +  map (Thm.symmetric o safe_mk_meta_eq) o Item_Net.content o #relator_eq o Data.get o Context.Proof
    1.37  
    1.38 -fun get_relator_eq_raw ctxt = ctxt
    1.39 -  |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
    1.40 +val get_relator_eq_raw = Item_Net.content o #relator_eq_raw o Data.get o Context.Proof
    1.41  
    1.42 -fun get_relator_domain ctxt = ctxt
    1.43 -  |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
    1.44 +val get_relator_domain = Item_Net.content o #relator_domain o Data.get o Context.Proof
    1.45  
    1.46 -fun get_pred_data ctxt = ctxt
    1.47 -  |> (#pred_data o Data.get o Context.Proof)
    1.48 +val get_pred_data = #pred_data o Data.get o Context.Proof
    1.49  
    1.50  fun map_data f1 f2 f3 f4 f5 f6 f7 f8
    1.51    { transfer_raw, known_frees, compound_lhs, compound_rhs,
    1.52 @@ -358,7 +349,7 @@
    1.53    in
    1.54      forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
    1.55    end
    1.56 -    handle TERM _ => thm
    1.57 +  handle TERM _ => thm
    1.58  
    1.59  fun abstract_domains_transfer ctxt thm =
    1.60    let
    1.61 @@ -404,14 +395,14 @@
    1.62  
    1.63  (** Adding transfer domain rules **)
    1.64  
    1.65 -fun prep_transfer_domain_thm ctxt thm =
    1.66 -  (abstract_equalities_domain ctxt o detect_transfer_rules) thm
    1.67 +fun prep_transfer_domain_thm ctxt =
    1.68 +  abstract_equalities_domain ctxt o detect_transfer_rules
    1.69  
    1.70 -fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
    1.71 -  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    1.72 +fun add_transfer_domain_thm thm ctxt =
    1.73 +  (add_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    1.74  
    1.75 -fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
    1.76 -  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    1.77 +fun del_transfer_domain_thm thm ctxt =
    1.78 +  (del_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    1.79  
    1.80  (** Transfer proof method **)
    1.81  
    1.82 @@ -495,32 +486,26 @@
    1.83    end
    1.84  
    1.85  (* create a lambda term of the same shape as the given term *)
    1.86 -fun skeleton (is_atom : term -> bool) ctxt t =
    1.87 +fun skeleton is_atom =
    1.88    let
    1.89      fun dummy ctxt =
    1.90 -      let
    1.91 -        val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
    1.92 -      in
    1.93 -        (Free (c, dummyT), ctxt)
    1.94 -      end
    1.95 -    fun go (Bound i) ctxt = (Bound i, ctxt)
    1.96 -      | go (Abs (x, _, t)) ctxt =
    1.97 -        let
    1.98 -          val (t', ctxt) = go t ctxt
    1.99 -        in
   1.100 -          (Abs (x, dummyT, t'), ctxt)
   1.101 -        end
   1.102 -      | go (tu as (t $ u)) ctxt =
   1.103 -        if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
   1.104 -        let
   1.105 -          val (t', ctxt) = go t ctxt
   1.106 -          val (u', ctxt) = go u ctxt
   1.107 -        in
   1.108 -          (t' $ u', ctxt)
   1.109 -        end
   1.110 -      | go _ ctxt = dummy ctxt
   1.111 +      let val (c, ctxt') = yield_singleton Variable.variant_fixes "a" ctxt
   1.112 +      in (Free (c, dummyT), ctxt') end
   1.113 +    fun skel (Bound i) ctxt = (Bound i, ctxt)
   1.114 +      | skel (Abs (x, _, t)) ctxt =
   1.115 +          let val (t', ctxt) = skel t ctxt
   1.116 +          in (Abs (x, dummyT, t'), ctxt) end
   1.117 +      | skel (tu as t $ u) ctxt =
   1.118 +          if is_atom tu andalso not (Term.is_open tu) then dummy ctxt
   1.119 +          else
   1.120 +            let
   1.121 +              val (t', ctxt) = skel t ctxt
   1.122 +              val (u', ctxt) = skel u ctxt
   1.123 +            in (t' $ u', ctxt) end
   1.124 +      | skel _ ctxt = dummy ctxt
   1.125    in
   1.126 -    go t ctxt |> fst |> Syntax.check_term ctxt
   1.127 +    fn ctxt => fn t =>
   1.128 +      fst (skel t ctxt) |> Syntax.check_term ctxt  (* FIXME avoid syntax operation!? *)
   1.129    end
   1.130  
   1.131  (** Monotonicity analysis **)
   1.132 @@ -580,7 +565,7 @@
   1.133  fun matches_list ctxt term =
   1.134    is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
   1.135  
   1.136 -fun transfer_rule_of_term ctxt equiv t : thm =
   1.137 +fun transfer_rule_of_term ctxt equiv t =
   1.138    let
   1.139      val compound_rhs = get_compound_rhs ctxt
   1.140      fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
   1.141 @@ -599,11 +584,11 @@
   1.142        ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   1.143    in
   1.144      thm
   1.145 -      |> Thm.generalize (tfrees, rnames @ frees) idx
   1.146 -      |> Thm.instantiate (map tinst binsts, map inst binsts)
   1.147 +    |> Thm.generalize (tfrees, rnames @ frees) idx
   1.148 +    |> Thm.instantiate (map tinst binsts, map inst binsts)
   1.149    end
   1.150  
   1.151 -fun transfer_rule_of_lhs ctxt t : thm =
   1.152 +fun transfer_rule_of_lhs ctxt t =
   1.153    let
   1.154      val compound_lhs = get_compound_lhs ctxt
   1.155      fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
   1.156 @@ -622,8 +607,8 @@
   1.157        ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   1.158    in
   1.159      thm
   1.160 -      |> Thm.generalize (tfrees, rnames @ frees) idx
   1.161 -      |> Thm.instantiate (map tinst binsts, map inst binsts)
   1.162 +    |> Thm.generalize (tfrees, rnames @ frees) idx
   1.163 +    |> Thm.instantiate (map tinst binsts, map inst binsts)
   1.164    end
   1.165  
   1.166  fun eq_rules_tac ctxt eq_rules =
   1.167 @@ -719,11 +704,8 @@
   1.168  
   1.169  fun transferred ctxt extra_rules thm =
   1.170    let
   1.171 -    val start_rule = @{thm transfer_start}
   1.172 -    val start_rule' = @{thm transfer_start'}
   1.173      val rules = extra_rules @ get_transfer_raw ctxt
   1.174      val eq_rules = get_relator_eq_raw ctxt
   1.175 -    val err_msg = "Transfer failed to convert goal to an object-logic formula"
   1.176      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   1.177      val thm1 = Drule.forall_intr_vars thm
   1.178      val instT =
   1.179 @@ -733,24 +715,22 @@
   1.180        |> Thm.instantiate (instT, [])
   1.181        |> Raw_Simplifier.rewrite_rule ctxt pre_simps
   1.182      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
   1.183 -    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   1.184 -    val rule = transfer_rule_of_lhs ctxt' t
   1.185 -    val tac =
   1.186 -      resolve_tac ctxt' [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
   1.187 -      (resolve_tac ctxt' [rule]
   1.188 -        THEN_ALL_NEW
   1.189 -          (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   1.190 -            THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
   1.191 -        handle TERM (_, ts) => raise TERM (err_msg, ts)
   1.192 -    val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>)))
   1.193 -    val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
   1.194 -    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
   1.195 +    val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2))
   1.196    in
   1.197 -    thm3
   1.198 -      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   1.199 -      |> Simplifier.norm_hhf ctxt'
   1.200 -      |> Drule.generalize (tnames, [])
   1.201 -      |> Drule.zero_var_indexes
   1.202 +    Goal.prove_internal ctxt' []
   1.203 +      (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>))))
   1.204 +      (fn _ =>
   1.205 +        resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN
   1.206 +        (resolve_tac ctxt' [rule]
   1.207 +          THEN_ALL_NEW
   1.208 +            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   1.209 +              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
   1.210 +          handle TERM (_, ts) =>
   1.211 +            raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
   1.212 +    |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   1.213 +    |> Simplifier.norm_hhf ctxt'
   1.214 +    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
   1.215 +    |> Drule.zero_var_indexes
   1.216    end
   1.217  (*
   1.218      handle THM _ => thm
   1.219 @@ -758,10 +738,8 @@
   1.220  
   1.221  fun untransferred ctxt extra_rules thm =
   1.222    let
   1.223 -    val start_rule = @{thm untransfer_start}
   1.224      val rules = extra_rules @ get_transfer_raw ctxt
   1.225      val eq_rules = get_relator_eq_raw ctxt
   1.226 -    val err_msg = "Transfer failed to convert goal to an object-logic formula"
   1.227      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   1.228      val thm1 = Drule.forall_intr_vars thm
   1.229      val instT =
   1.230 @@ -773,22 +751,21 @@
   1.231      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
   1.232      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   1.233      val rule = transfer_rule_of_term ctxt' true t
   1.234 -    val tac =
   1.235 -      resolve_tac ctxt' [thm2 RS start_rule] 1 THEN
   1.236 -      (resolve_tac ctxt' [rule]
   1.237 -        THEN_ALL_NEW
   1.238 -          (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   1.239 -            THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
   1.240 -        handle TERM (_, ts) => raise TERM (err_msg, ts)
   1.241 -    val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>)))
   1.242 -    val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
   1.243 -    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
   1.244    in
   1.245 -    thm3
   1.246 -      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   1.247 -      |> Simplifier.norm_hhf ctxt'
   1.248 -      |> Drule.generalize (tnames, [])
   1.249 -      |> Drule.zero_var_indexes
   1.250 +    Goal.prove_internal ctxt' []
   1.251 +      (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>))))
   1.252 +      (fn _ =>
   1.253 +        resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN
   1.254 +        (resolve_tac ctxt' [rule]
   1.255 +          THEN_ALL_NEW
   1.256 +            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   1.257 +              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
   1.258 +          handle TERM (_, ts) =>
   1.259 +            raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
   1.260 +    |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   1.261 +    |> Simplifier.norm_hhf ctxt'
   1.262 +    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
   1.263 +    |> Drule.zero_var_indexes
   1.264    end
   1.265  
   1.266  (** Methods and attributes **)
   1.267 @@ -863,7 +840,8 @@
   1.268      map_pred_data' morph_thm morph_thm (map morph_thm)
   1.269    end
   1.270  
   1.271 -fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
   1.272 +fun lookup_pred_data ctxt type_name =
   1.273 +  Symtab.lookup (get_pred_data ctxt) type_name
   1.274    |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt))
   1.275  
   1.276  fun update_pred_data type_name qinfo ctxt =
     2.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Jun 04 13:09:24 2019 +0200
     2.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Jun 04 13:14:17 2019 +0200
     2.3 @@ -72,55 +72,56 @@
     2.4        constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
     2.5        |> head_of |> fst o dest_Const
     2.6      val live = live_of_bnf bnf
     2.7 -    val (((As, Bs), Ds), ctxt) = ctxt
     2.8 +    val (((As, Bs), Ds), ctxt') = ctxt
     2.9        |> mk_TFrees live
    2.10        ||>> mk_TFrees live
    2.11        ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
    2.12  
    2.13      val relator = mk_rel_of_bnf Ds As Bs bnf
    2.14      val relsT = map2 mk_pred2T As Bs
    2.15 -    val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
    2.16 +    val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt'
    2.17      val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
    2.18      val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
    2.19      val goal = Logic.list_implies (assms, concl)
    2.20    in
    2.21 -    (goal, ctxt)
    2.22 +    (goal, ctxt'')
    2.23    end
    2.24  
    2.25  fun prove_relation_side_constraint ctxt bnf constraint_def =
    2.26    let
    2.27 -    val old_ctxt = ctxt
    2.28 -    val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
    2.29 -    val thm = Goal.prove_sorry ctxt [] [] goal
    2.30 -      (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
    2.31 -      |> Thm.close_derivation
    2.32 +    val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def
    2.33    in
    2.34 -    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
    2.35 +    Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
    2.36 +      side_constraint_tac bnf [constraint_def] goal_ctxt 1)
    2.37 +    |> Thm.close_derivation
    2.38 +    |> singleton (Variable.export ctxt' ctxt)
    2.39 +    |> Drule.zero_var_indexes
    2.40    end
    2.41  
    2.42  fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
    2.43    let
    2.44 -    val old_ctxt = ctxt
    2.45 -    val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
    2.46 -    val thm = Goal.prove_sorry ctxt [] [] goal
    2.47 -      (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
    2.48 -      |> Thm.close_derivation
    2.49 +    val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def
    2.50    in
    2.51 -    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
    2.52 +    Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
    2.53 +      bi_constraint_tac constraint_def side_constraints goal_ctxt 1)
    2.54 +    |> Thm.close_derivation
    2.55 +    |> singleton (Variable.export ctxt' ctxt)
    2.56 +    |> Drule.zero_var_indexes
    2.57    end
    2.58  
    2.59 -val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
    2.60 +val defs =
    2.61 + [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
    2.62    ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
    2.63  
    2.64 -fun prove_relation_constraints bnf lthy =
    2.65 +fun prove_relation_constraints bnf ctxt =
    2.66    let
    2.67      val transfer_attr = @{attributes [transfer_rule]}
    2.68      val Tname = base_name_of_bnf bnf
    2.69  
    2.70 -    val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
    2.71 -    val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
    2.72 +    val defs = map (apsnd (prove_relation_side_constraint ctxt bnf)) defs
    2.73 +    val bi_total = prove_relation_bi_constraint ctxt bnf @{thm bi_total_alt_def}
    2.74        [snd (nth defs 0), snd (nth defs 1)]
    2.75 -    val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
    2.76 +    val bi_unique = prove_relation_bi_constraint ctxt bnf @{thm bi_unique_alt_def}
    2.77        [snd (nth defs 2), snd (nth defs 3)]
    2.78      val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
    2.79    in
    2.80 @@ -174,23 +175,23 @@
    2.81  fun prove_Domainp_rel ctxt bnf pred_def =
    2.82    let
    2.83      val live = live_of_bnf bnf
    2.84 -    val old_ctxt = ctxt
    2.85 -    val (((As, Bs), Ds), ctxt) = ctxt
    2.86 +    val (((As, Bs), Ds), ctxt') = ctxt
    2.87        |> mk_TFrees live
    2.88        ||>> mk_TFrees live
    2.89        ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
    2.90  
    2.91      val relator = mk_rel_of_bnf Ds As Bs bnf
    2.92      val relsT = map2 mk_pred2T As Bs
    2.93 -    val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
    2.94 +    val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt'
    2.95      val lhs = mk_Domainp (list_comb (relator, args))
    2.96      val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args)
    2.97      val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
    2.98 -    val thm = Goal.prove_sorry ctxt [] [] goal
    2.99 -      (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
   2.100 -      |> Thm.close_derivation
   2.101    in
   2.102 -    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
   2.103 +    Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} =>
   2.104 +      Domainp_tac bnf pred_def goal_ctxt 1)
   2.105 +    |> Thm.close_derivation
   2.106 +    |> singleton (Variable.export ctxt'' ctxt)
   2.107 +    |> Drule.zero_var_indexes
   2.108    end
   2.109  
   2.110  fun predicator bnf lthy =
   2.111 @@ -232,8 +233,8 @@
   2.112  
   2.113  (* simplification rules for the predicator *)
   2.114  
   2.115 -fun lookup_defined_pred_data lthy name =
   2.116 -  case Transfer.lookup_pred_data lthy name of
   2.117 +fun lookup_defined_pred_data ctxt name =
   2.118 +  case Transfer.lookup_pred_data ctxt name of
   2.119      SOME data => data
   2.120    | NONE => raise NO_PRED_DATA ()
   2.121