src/HOL/Tools/Function/induction_schema.ML
changeset 35625 9c818cab0dd0
parent 34232 36a2a3029fd3
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4        |> fold_rev (curry Logic.mk_implies) Cs
     1.5        |> fold_rev (Logic.all o Free) ws
     1.6        |> term_conv thy ind_atomize
     1.7 -      |> ObjectLogic.drop_judgment thy
     1.8 +      |> Object_Logic.drop_judgment thy
     1.9        |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
    1.10    in
    1.11      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)