src/Tools/code/code_funcgr.ML

     val ct'' = Thm.rhs_of thm6;
     val c_exprs = consts_of ct'';
     val drop = drop_classes thy tfrees;
     val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
     val funcgr'' = ensure_consts thy algebra instdefs funcgr';
-  in (f drop thm5 funcgr'' ct'' , funcgr'') end;
+  in (f drop thm5 funcgr'' ct'', funcgr'') end;
 
 fun raw_eval_conv thy conv =
   let
     fun conv' drop_classes thm1 funcgr ct =
       let