src/HOL/Library/refute.ML
changeset 59582 0fbed69ff081
parent 59352 63c02d051661
child 59936 b8ffc3dc9e24
     1.1 --- a/src/HOL/Library/refute.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -1202,13 +1202,13 @@
     1.4  
     1.5  fun refute_goal ctxt params th i =
     1.6    let
     1.7 -    val t = th |> prop_of
     1.8 +    val t = th |> Thm.prop_of
     1.9    in
    1.10      if Logic.count_prems t = 0 then
    1.11        (writeln "No subgoal!"; "none")
    1.12      else
    1.13        let
    1.14 -        val assms = map term_of (Assumption.all_assms_of ctxt)
    1.15 +        val assms = map Thm.term_of (Assumption.all_assms_of ctxt)
    1.16          val (t, frees) = Logic.goal_params t i
    1.17        in
    1.18          refute_term ctxt params assms (subst_bounds (frees, t))