src/HOL/Tools/inductive_realizer.ML
changeset 36744 6e1f3d609a68
parent 36692 54b64d4ad524
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 08 17:10:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 08 16:53:53 2010 +0200
     1.3 @@ -408,7 +408,7 @@
     1.4        in
     1.5          Extraction.add_realizers_i
     1.6            (map (fn (((ind, corr), rlz), r) =>
     1.7 -              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
     1.8 +              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
     1.9              realizers @ (case realizers of
    1.10               [(((ind, corr), rlz), r)] =>
    1.11                 [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",