src/Pure/Isar/code.ML
changeset 28353 40306cc4d16a
parent 28350 715163ec93c0
child 28359 bd4750bcb4e6
     1.1 --- a/src/Pure/Isar/code.ML	Thu Sep 25 10:17:23 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 25 11:14:01 2008 +0200
     1.3 @@ -773,13 +773,18 @@
     1.4  local
     1.5  
     1.6  fun apply_functrans thy [] = []
     1.7 -  | apply_functrans thy (thms as thm :: _) =
     1.8 +  | apply_functrans thy (thms as (thm, _) :: _) =
     1.9        let
    1.10          val const = const_of_func thy thm;
    1.11          val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
    1.12            o the_thmproc o the_exec) thy;
    1.13 -        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) thms;
    1.14 -      in certify_const thy const thms' end;
    1.15 +        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) (map fst thms);
    1.16 +        val thms'' = certify_const thy const thms';
    1.17 +        val linears = map snd thms;
    1.18 +      in (*FIXME temporary workaround*) if length thms'' = length linears
    1.19 +        then thms'' ~~ linears
    1.20 +        else map (rpair true) thms''
    1.21 +      end;
    1.22  
    1.23  fun rhs_conv conv thm =
    1.24    let
    1.25 @@ -801,10 +806,10 @@
    1.26    in
    1.27      thms
    1.28      |> apply_functrans thy
    1.29 -    |> map (Code_Unit.rewrite_func pre)
    1.30 +    |> (map o apfst) (Code_Unit.rewrite_func pre)
    1.31      (*FIXME - must check here: rewrite rule, defining equation, proper constant *)
    1.32 -    |> map (AxClass.unoverload thy)
    1.33 -    |> common_typ_funcs
    1.34 +    |> (map o apfst) (AxClass.unoverload thy)
    1.35 +    |> burrow_fst common_typ_funcs
    1.36    end;
    1.37  
    1.38  
    1.39 @@ -858,7 +863,7 @@
    1.40        o ObjectLogic.drop_judgment thy o Thm.plain_prop_of o fst);
    1.41    in
    1.42      get_funcs thy const
    1.43 -    |> burrow_fst (preprocess thy)
    1.44 +    |> preprocess thy
    1.45      |> drop_refl thy
    1.46    end;
    1.47