src/Pure/Thy/term_style.ML
changeset 41685 e29ea98a76ce
parent 36950 75b8f26f2f07
child 41686 d8efc2490b8e
equal deleted inserted replaced
41677:fa0da47131d2 41685:e29ea98a76ce
    92     if i <= length prems then nth prems (i - 1)
    92     if i <= length prems then nth prems (i - 1)
    93     else error ("Not enough premises for prem" ^ i_str ^
    93     else error ("Not enough premises for prem" ^ i_str ^
    94       " in propositon: " ^ Syntax.string_of_term ctxt t)
    94       " in propositon: " ^ Syntax.string_of_term ctxt t)
    95   end);
    95   end);
    96 
    96 
       
    97 fun isub_symbols (d :: s :: ss) =
       
    98       if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
       
    99       then d :: "\\<^isub>" :: isub_symbols (s :: ss)
       
   100       else d :: s :: ss
       
   101   | isub_symbols cs = cs;
       
   102 
       
   103 val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
       
   104 
       
   105 fun isub_term (Free (n, T)) = Free (isub_name n, T)
       
   106   | isub_term (Var ((n, idx), T)) =
       
   107       if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
       
   108       else Var ((isub_name n, 0), T)
       
   109   | isub_term (t $ u) = isub_term t $ isub_term u
       
   110   | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
       
   111   | isub_term t = t;
       
   112 
       
   113 val style_isub = Scan.succeed (K isub_term);
       
   114 
    97 val _ = Context.>> (Context.map_theory
   115 val _ = Context.>> (Context.map_theory
    98  (setup "lhs" (style_lhs_rhs fst) #>
   116  (setup "lhs" (style_lhs_rhs fst) #>
    99   setup "rhs" (style_lhs_rhs snd) #>
   117   setup "rhs" (style_lhs_rhs snd) #>
   100   setup "prem" style_prem #>
   118   setup "prem" style_prem #>
   101   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
   119   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
       
   120   setup "isub" style_isub #>
   102   setup "prem1" (style_parm_premise 1) #>
   121   setup "prem1" (style_parm_premise 1) #>
   103   setup "prem2" (style_parm_premise 2) #>
   122   setup "prem2" (style_parm_premise 2) #>
   104   setup "prem3" (style_parm_premise 3) #>
   123   setup "prem3" (style_parm_premise 3) #>
   105   setup "prem4" (style_parm_premise 4) #>
   124   setup "prem4" (style_parm_premise 4) #>
   106   setup "prem5" (style_parm_premise 5) #>
   125   setup "prem5" (style_parm_premise 5) #>