src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
changeset 54180 1753c57eb16c
parent 54178 d6dc359426b7
child 54200 064f88a41096
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 09:14:05 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 09:31:19 2013 +0200
     1.3 @@ -896,7 +896,7 @@
     1.4      val exclss'' = exclss' |> map (map (fn (idx, t) =>
     1.5        (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (excl_tac idx), t))));
     1.6      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     1.7 -    val (obligation_idxss, goalss) = exclss''
     1.8 +    val (goal_idxss, goalss) = exclss''
     1.9        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
    1.10        |> split_list o map split_list;
    1.11  
    1.12 @@ -904,7 +904,7 @@
    1.13        let
    1.14          val def_thms = map (snd o snd) def_thms';
    1.15  
    1.16 -        val exclss' = map (op ~~) (obligation_idxss ~~ thmss');
    1.17 +        val exclss' = map (op ~~) (goal_idxss ~~ thmss');
    1.18          fun mk_exclsss excls n =
    1.19            (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
    1.20            |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));