src/HOL/Tools/res_axioms.ML
changeset 22596 d0d2af4db18f
parent 22516 c986140356b8
child 22644 f10465ee7aa2
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Apr 04 20:22:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Apr 04 23:29:33 2007 +0200
     1.3 @@ -394,10 +394,10 @@
     1.4    let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
     1.5        val (ch, frees) = c_variant_abs_multi (rhs, [])
     1.6        val (chilbert,cabs) = Thm.dest_comb ch
     1.7 -      val {sign,t, ...} = rep_cterm chilbert
     1.8 +      val {thy,t, ...} = rep_cterm chilbert
     1.9        val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
    1.10                        | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
    1.11 -      val cex = Thm.cterm_of sign (HOLogic.exists_const T)
    1.12 +      val cex = Thm.cterm_of thy (HOLogic.exists_const T)
    1.13        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
    1.14        and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
    1.15        fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1