Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment out code that's not ready
authorblanchet
Sat, 08 Sep 2012 21:04:26 +0200
changeset 49216 e6fc5a6b152d
parent 49215 1c5d6e2eb0c6
child 49217 0c9546fc789f
comment out code that's not ready
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -501,6 +501,7 @@
     fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, vs, xsss, ctr_defss, coiter_defs,
         corec_defs), lthy) =
       let
+(* NOTYET
         val gcoiters = map (lists_bmoc pgss) coiters;
         val hcorecs = map (lists_bmoc phss) corecs;
 
@@ -540,8 +541,9 @@
             map2 (fn b => fn thms =>
                 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
               bs thmss);
+*)
       in
-        lthy |> Local_Theory.notes notes |> snd
+        lthy (* NOTYET |> Local_Theory.notes notes |> snd *)
       end;
 
     val lthy' = lthy
isabelle