src/HOL/Data_Structures/Define_Time_Function.ML

       constc {ctxt = ctxt, origins = origin, f = walk ctxt origin conv} c
 fun Ifunc (wctxt: term wctxt) t args = list_comb (#f wctxt t,map (#f wctxt) args)
 val Iconst = K I
 fun Iif (wctxt: term wctxt) T cond tt tf =
   Const (@{const_name "HOL.If"}, T) $ (#f wctxt cond) $ (#f wctxt tt) $ (#f wctxt tf)
-fun Icase (wctxt: term wctxt) t cs = list_comb (#f wctxt t,map (#f wctxt) cs)
+fun Icase (wctxt: term wctxt) t cs = list_comb
+  (#f wctxt t,map (fn c => c |> Term.strip_abs_eta (c |> fastype_of |> strip_type |> fst |> length) ||> #f wctxt |> list_abs) cs)
 fun Ilet (wctxt: term wctxt) lT exp abs t =
-  Const (@{const_name "HOL.Let"},lT) $ (#f wctxt exp) $ list_abs (abs, #f wctxt t)
+  Const (@{const_name "HOL.Let"}, lT) $ (#f wctxt exp) $ list_abs (abs, #f wctxt t)
 
 (* 1. Fix all terms *)
 (* Exchange Var in types and terms to Free *)
 fun freeTerms (Var(ixn,T)) = Free (fst ixn, T)
   | freeTerms t = t

 fun fixTerms ctxt (term: term list) (fixedNum: int) (t as pT $ (eq $ l $ r)) =
   let
     val _ = check_args "args" (strip_comb (get_l t))
     val l' = shortApp fixedNum (strip_comb l) |> list_comb
     val shortOriginFunc' = shortOriginFunc (term |> map (fst o strip_comb)) fixedNum
+    val consts = Proof_Context.consts_of ctxt
+    val net = Consts.revert_abbrevs consts ["internal"] |> hd |> Item_Net.content
+                (* filter out consts *)
+              |> filter (is_Const o fst o strip_comb o fst)
+                (* filter out abbreviations for locales *)
+              |> filter (fn n => "local"
+                  = (n |> snd |> strip_comb |> fst |> dest_Const_name |> split_name |> hd))
+              |> filter (fn n => (n |> fst |> strip_comb |> fst |> dest_Const_name |> split_name |> List.last) =
+                (n |> snd |> strip_comb |> fst |> dest_Const_name |> split_name |> List.last))
+              |> map (fst #> strip_comb #>> dest_Const_name ##> length)
+    fun n_abbrev (Const (nm,_)) =
+    let
+      val f = filter (fn n => fst n = nm) net
+    in
+      if length f >= 1 then f |> hd |> snd else 0
+    end
+      | n_abbrev _ = 0
     val r' = walk ctxt term {
           funcc = (fn wctxt => fn t => fn args =>
-              (check_args "func" (t,args); (#f wctxt t, map (#f wctxt) args) |> shortOriginFunc' |> list_comb)),
+            let
+              val n_abb = n_abbrev t
+              val t = case t of Const (nm,T) => Const (nm, T |> strip_type |>> drop n_abb |> (op --->))
+                              | t => t
+              val args = drop n_abb args           
+            in
+              (check_args "func" (t,args);
+               (#f wctxt t, map (#f wctxt) args) |> shortOriginFunc' |> list_comb)
+            end),
           constc = fn wctxt => map_abs (#f wctxt),
           ifc = Iif,
           casec = fixCasec,
           letc = (fn wctxt => fn expT => fn exp => fn abs => fn t =>
               (Const (@{const_name "HOL.Let"},expT) $ (#f wctxt exp) $ list_abs (abs, #f wctxt t)))

             handle (ERROR _) => NONE
         of SOME _ => error ("Timing function already declared: " ^ (Term.term_name (hd term)))
          | NONE => ()
 
     (* Number of terms fixed by locale *)
-    val fixedNum = term
-      |> hd
+    val fixedNum = term |> hd
       |> strip_comb |> snd
       |> length
 
     (* 1. Fix all terms *)
     (* Exchange Var in types and terms to Free and check constraints *)