src/Tools/induct.ML
changeset 45156 a9b6c2ea7bec
parent 45132 09de0d0de645
child 45328 e5b33eecbf6e
     1.1 --- a/src/Tools/induct.ML	Sun Oct 16 16:56:01 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Sun Oct 16 18:48:30 2011 +0200
     1.3 @@ -642,9 +642,9 @@
     1.4  local
     1.5  
     1.6  fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
     1.7 -  | goal_prefix 0 _ = Term.dummy_pattern propT
     1.8 +  | goal_prefix 0 _ = Term.dummy_prop
     1.9    | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
    1.10 -  | goal_prefix _ _ = Term.dummy_pattern propT;
    1.11 +  | goal_prefix _ _ = Term.dummy_prop;
    1.12  
    1.13  fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
    1.14    | goal_params 0 _ = 0