src/HOL/Library/reflection.ML
changeset 42368 3b8498ac2314
parent 42361 23f352990944
child 42426 7ec150fcf3dc
     1.1 --- a/src/HOL/Library/reflection.ML	Sat Apr 16 20:30:44 2011 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Sat Apr 16 20:49:48 2011 +0200
     1.3 @@ -298,23 +298,19 @@
     1.4               (simplify (HOL_basic_ss addsimps [rth]) th)
     1.5    end
     1.6  
     1.7 -fun genreify_tac ctxt eqs to i = (fn st =>
     1.8 +fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
     1.9    let
    1.10 -    fun P () = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1))
    1.11 -    val t = (case to of NONE => P () | SOME x => x)
    1.12 -    val th = (genreif ctxt eqs t) RS ssubst
    1.13 -  in rtac th i st
    1.14 -  end);
    1.15 +    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
    1.16 +    val th = genreif ctxt eqs t RS ssubst
    1.17 +  in rtac th i end);
    1.18  
    1.19      (* Reflection calls reification and uses the correctness *)
    1.20          (* theorem assumed to be the dead of the list *)
    1.21 -fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
    1.22 +fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
    1.23    let
    1.24 -    val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
    1.25 -    val t = the_default P to;
    1.26 -    val th = genreflect ctxt conv corr_thms raw_eqs t
    1.27 -      RS ssubst;
    1.28 -  in (rtac th i THEN TRY(rtac TrueI i)) st end);
    1.29 +    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
    1.30 +    val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
    1.31 +  in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
    1.32  
    1.33  fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
    1.34    (*FIXME why Codegen.evaluation_conv?  very specific...*)