src/Pure/Thy/term_style.ML
changeset 41686 d8efc2490b8e
parent 41685 e29ea98a76ce
child 42016 3b6826b3ed37
equal deleted inserted replaced
41685:e29ea98a76ce 41686:d8efc2490b8e
   108       else Var ((isub_name n, 0), T)
   108       else Var ((isub_name n, 0), T)
   109   | isub_term (t $ u) = isub_term t $ isub_term u
   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)
   110   | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
   111   | isub_term t = t;
   111   | isub_term t = t;
   112 
   112 
   113 val style_isub = Scan.succeed (K isub_term);
       
   114 
       
   115 val _ = Context.>> (Context.map_theory
   113 val _ = Context.>> (Context.map_theory
   116  (setup "lhs" (style_lhs_rhs fst) #>
   114  (setup "lhs" (style_lhs_rhs fst) #>
   117   setup "rhs" (style_lhs_rhs snd) #>
   115   setup "rhs" (style_lhs_rhs snd) #>
   118   setup "prem" style_prem #>
   116   setup "prem" style_prem #>
   119   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
   117   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
   120   setup "isub" style_isub #>
   118   setup "isub" (Scan.succeed (K isub_term)) #>
   121   setup "prem1" (style_parm_premise 1) #>
   119   setup "prem1" (style_parm_premise 1) #>
   122   setup "prem2" (style_parm_premise 2) #>
   120   setup "prem2" (style_parm_premise 2) #>
   123   setup "prem3" (style_parm_premise 3) #>
   121   setup "prem3" (style_parm_premise 3) #>
   124   setup "prem4" (style_parm_premise 4) #>
   122   setup "prem4" (style_parm_premise 4) #>
   125   setup "prem5" (style_parm_premise 5) #>
   123   setup "prem5" (style_parm_premise 5) #>