src/Tools/induct.ML
changeset 47060 e2741ec9ae36
parent 46961 5c6955f487e5
child 49660 de49d9b4d7bc
     1.1 --- a/src/Tools/induct.ML	Tue Mar 20 21:37:31 2012 +0100
     1.2 +++ b/src/Tools/induct.ML	Wed Mar 21 11:00:34 2012 +0100
     1.3 @@ -104,12 +104,12 @@
     1.4  
     1.5  val mk_var = Net.encode_type o #2 o Term.dest_Var;
     1.6  
     1.7 -fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
     1.8 +fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
     1.9    raise THM ("No variables in conclusion of rule", 0, [thm]);
    1.10  
    1.11  in
    1.12  
    1.13 -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
    1.14 +fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
    1.15    raise THM ("No variables in major premise of rule", 0, [thm]);
    1.16  
    1.17  val left_var_concl = concl_var hd;