src/HOL/Nominal/nominal_inductive.ML
changeset 39159 0dec18004e75
parent 38795 848be46708dc
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -30,10 +30,10 @@
     1.4  
     1.5  fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     1.6  
     1.7 -val fresh_prod = thm "fresh_prod";
     1.8 +val fresh_prod = @{thm fresh_prod};
     1.9  
    1.10 -val perm_bool = mk_meta_eq (thm "perm_bool");
    1.11 -val perm_boolI = thm "perm_boolI";
    1.12 +val perm_bool = mk_meta_eq @{thm perm_bool};
    1.13 +val perm_boolI = @{thm perm_boolI};
    1.14  val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
    1.15    (Drule.strip_imp_concl (cprop_of perm_boolI))));
    1.16