src/HOL/Tools/Meson/meson.ML
changeset 60358 aebfbcab1eb8
parent 59632 5980e75a204e
child 60362 befdc10ebb42
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -41,8 +41,8 @@
     1.4    val prolog_step_tac': Proof.context -> thm list -> int -> tactic
     1.5    val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
     1.6    val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
     1.7 -  val make_meta_clause: thm -> thm
     1.8 -  val make_meta_clauses: thm list -> thm list
     1.9 +  val make_meta_clause: Proof.context -> thm -> thm
    1.10 +  val make_meta_clauses: Proof.context -> thm list -> thm list
    1.11    val meson_tac: Proof.context -> thm list -> int -> tactic
    1.12  end
    1.13  
    1.14 @@ -787,15 +787,15 @@
    1.15      th RS notEfalse handle THM _ => th RS notEfalse';
    1.16  
    1.17  (*Converting one theorem from a disjunction to a meta-level clause*)
    1.18 -fun make_meta_clause th =
    1.19 -  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
    1.20 +fun make_meta_clause ctxt th =
    1.21 +  let val (fth, thaw) = Misc_Legacy.freeze_thaw_robust ctxt th
    1.22    in  
    1.23        (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
    1.24         negated_asm_of_head o make_horn resolution_clause_rules) fth
    1.25    end;
    1.26  
    1.27 -fun make_meta_clauses ths =
    1.28 +fun make_meta_clauses ctxt ths =
    1.29      name_thms "MClause#"
    1.30 -      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    1.31 +      (distinct Thm.eq_thm_prop (map (make_meta_clause ctxt) ths));
    1.32  
    1.33  end;