(temporary workaround)
authorhaftmann
Thu Sep 25 11:14:01 2008 +0200 (2008-09-25)
changeset 2835340306cc4d16a
parent 28352 cab797b79421
child 28354 c5fe7372ae4e
(temporary workaround)
src/HOL/ex/ROOT.ML
src/Pure/Isar/code.ML
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Sep 25 10:17:23 2008 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 25 11:14:01 2008 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  ];
     1.5  
     1.6  no_document use_thy "Codegenerator";
     1.7 -(*no_document use_thy "Codegenerator_Pretty";*)
     1.8 +no_document use_thy "Codegenerator_Pretty";
     1.9  
    1.10  use_thys [
    1.11    "Numeral",
     2.1 --- a/src/Pure/Isar/code.ML	Thu Sep 25 10:17:23 2008 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 25 11:14:01 2008 +0200
     2.3 @@ -773,13 +773,18 @@
     2.4  local
     2.5  
     2.6  fun apply_functrans thy [] = []
     2.7 -  | apply_functrans thy (thms as thm :: _) =
     2.8 +  | apply_functrans thy (thms as (thm, _) :: _) =
     2.9        let
    2.10          val const = const_of_func thy thm;
    2.11          val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
    2.12            o the_thmproc o the_exec) thy;
    2.13 -        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) thms;
    2.14 -      in certify_const thy const thms' end;
    2.15 +        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) (map fst thms);
    2.16 +        val thms'' = certify_const thy const thms';
    2.17 +        val linears = map snd thms;
    2.18 +      in (*FIXME temporary workaround*) if length thms'' = length linears
    2.19 +        then thms'' ~~ linears
    2.20 +        else map (rpair true) thms''
    2.21 +      end;
    2.22  
    2.23  fun rhs_conv conv thm =
    2.24    let
    2.25 @@ -801,10 +806,10 @@
    2.26    in
    2.27      thms
    2.28      |> apply_functrans thy
    2.29 -    |> map (Code_Unit.rewrite_func pre)
    2.30 +    |> (map o apfst) (Code_Unit.rewrite_func pre)
    2.31      (*FIXME - must check here: rewrite rule, defining equation, proper constant *)
    2.32 -    |> map (AxClass.unoverload thy)
    2.33 -    |> common_typ_funcs
    2.34 +    |> (map o apfst) (AxClass.unoverload thy)
    2.35 +    |> burrow_fst common_typ_funcs
    2.36    end;
    2.37  
    2.38  
    2.39 @@ -858,7 +863,7 @@
    2.40        o ObjectLogic.drop_judgment thy o Thm.plain_prop_of o fst);
    2.41    in
    2.42      get_funcs thy const
    2.43 -    |> burrow_fst (preprocess thy)
    2.44 +    |> preprocess thy
    2.45      |> drop_refl thy
    2.46    end;
    2.47