src/HOL/Nominal/nominal_fresh_fun.ML
changeset 30280 eb98b49ef835
parent 29265 5b4247055bd7
child 30364 577edc39b501
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 05 11:58:53 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 05 12:08:00 2009 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4   let 
     1.5     val thy = theory_of_thm thm;
     1.6  (* the parsing function returns a qualified name, we get back the base name *)
     1.7 -   val atom_basename = Sign.base_name atom_name;
     1.8 +   val atom_basename = NameSpace.base_name atom_name;
     1.9     val goal = List.nth(prems_of thm, i-1);
    1.10     val ps = Logic.strip_params goal;
    1.11     val Ts = rev (map snd ps);
    1.12 @@ -159,7 +159,7 @@
    1.13      NONE => all_tac thm
    1.14    | SOME atom_name  =>    
    1.15    let 
    1.16 -    val atom_basename = Sign.base_name atom_name;
    1.17 +    val atom_basename = NameSpace.base_name atom_name;
    1.18      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    1.19      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.20      fun inst_fresh vars params i st =