src/HOL/Tools/TFL/post.ML
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 54999 7859ed58c041
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -68,10 +68,11 @@
     1.4    |   _ => r RS P_imp_P_eq_True
     1.5  
     1.6  (*Is this the best way to invoke the simplifier??*)
     1.7 -fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
     1.8 +fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
     1.9  
    1.10  fun join_assums th =
    1.11    let val thy = Thm.theory_of_thm th
    1.12 +      val ctxt = Proof_Context.init_global thy
    1.13        val tych = cterm_of thy
    1.14        val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
    1.15        val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
    1.16 @@ -80,7 +81,7 @@
    1.17    in
    1.18      Rules.GEN_ALL
    1.19        (Rules.DISCH_ALL
    1.20 -         (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
    1.21 +         (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
    1.22    end
    1.23    val gen_all = USyntax.gen_all
    1.24  in
    1.25 @@ -139,7 +140,7 @@
    1.26     let
    1.27         val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
    1.28         val {rules,rows,TCs,full_pats_TCs} =
    1.29 -           Prim.post_definition congs (thy, (def, pats))
    1.30 +           Prim.post_definition congs thy ctxt (def, pats)
    1.31         val {lhs=f,rhs} = USyntax.dest_eq (concl def)
    1.32         val (_,[R,_]) = USyntax.strip_comb rhs
    1.33         val dummy = Prim.trace_thms "congs =" congs
    1.34 @@ -149,9 +150,9 @@
    1.35                 {f = f, R = R, rules = rules,
    1.36                  full_pats_TCs = full_pats_TCs,
    1.37                  TCs = TCs}
    1.38 -       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
    1.39 +       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
    1.40                          (Rules.CONJUNCTS rules)
    1.41 -         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
    1.42 +         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
    1.43          rules = ListPair.zip(rules', rows),
    1.44          tcs = (termination_goals rules') @ tcs}
    1.45     end
    1.46 @@ -170,7 +171,7 @@
    1.47      | solve_eq _ (th, [a], i) = [(a, i)]
    1.48      | solve_eq ctxt (th, splitths, i) =
    1.49        (writeln "Proving unsplit equation...";
    1.50 -      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
    1.51 +      [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
    1.52            (CaseSplit.splitto ctxt splitths th), i)])
    1.53        handle ERROR s => 
    1.54               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);