follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
authorblanchet
Tue, 18 Feb 2014 01:11:25 +0100
changeset 55540 892a425c5eaa
parent 55539 0819931d652d
child 55541 fd9ea8ae28f6
follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 22:54:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 01:11:25 2014 +0100
@@ -132,7 +132,7 @@
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
-    val {co_inducts = [induct], ...} :: _ = fp_sugars;
+    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
     val inducts = map (the_single o #co_inducts) fp_sugars;
 
     fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a