src/HOL/Tools/BNF/bnf_lfp.ML
changeset 62698 9d706e37ddab
parent 62689 9b8b3db6ac03
child 62721 f3248e77c960
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 22 13:32:40 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 22 13:44:50 2016 +0100
     1.3 @@ -1329,7 +1329,7 @@
     1.4          val vars = Variable.add_free_names lthy goal [];
     1.5        in
     1.6          (Goal.prove_sorry lthy vars [] goal
     1.7 -          (fn {context = ctxt, prems = _} => 
     1.8 +          (fn {context = ctxt, prems = _} =>
     1.9              mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
    1.10              Rep_inverses Abs_inverses Reps)
    1.11          |> Thm.close_derivation,